mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-26 18:45:33 +00:00
Code Activity

remove interpolation and duality dependencies

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-05-24 08:33:19 -07:00
parent d088a1b9f6
commit 4f5775c531
59 changed files with 3 additions and 26262 deletions
Download patch file Download diff file Expand all files Collapse all files

2
RELEASE_NOTES
View file

@ -35,7 +35,7 @@ Version 4.7.1
=============
- New requirements:
- uses stdbool and stdint as part of z3.h
- uses stdbool and stdint as part of z3.
- New features:
- none

5
src/CMakeLists.txt
View file

@ -12,7 +12,6 @@ set(Z3_API_HEADER_FILES_TO_SCAN
z3_rcf.h
z3_fixedpoint.h
z3_optimization.h
z3_interp.h
z3_fpa.h
z3_spacer.h
)
@ -63,7 +62,6 @@ add_subdirectory(sat/tactic)
add_subdirectory(tactic/arith)
add_subdirectory(nlsat/tactic)
add_subdirectory(ackermannization)
add_subdirectory(interp)
add_subdirectory(cmd_context)
add_subdirectory(cmd_context/extra_cmds)
add_subdirectory(parsers/smt2)
@ -79,7 +77,6 @@ add_subdirectory(tactic/bv)
add_subdirectory(smt/tactic)
add_subdirectory(tactic/sls)
add_subdirectory(qe)
add_subdirectory(duality)
add_subdirectory(muz/base)
add_subdirectory(muz/dataflow)
add_subdirectory(muz/transforms)
@ -89,7 +86,6 @@ add_subdirectory(muz/clp)
add_subdirectory(muz/tab)
add_subdirectory(muz/bmc)
add_subdirectory(muz/ddnf)
add_subdirectory(muz/duality)
add_subdirectory(muz/spacer)
add_subdirectory(muz/fp)
add_subdirectory(tactic/ufbv)
@ -159,7 +155,6 @@ set (libz3_public_headers
z3_fpa.h
z3.h
c++/z3++.h
z3_interp.h
z3_macros.h
z3_optimization.h
z3_polynomial.h

2
src/api/CMakeLists.txt
View file

@ -48,7 +48,6 @@ z3_add_component(api
api_datatype.cpp
api_fpa.cpp
api_goal.cpp
api_interp.cpp
api_log.cpp
api_model.cpp
api_numeral.cpp
@ -67,7 +66,6 @@ z3_add_component(api
z3_replayer.cpp
${full_path_generated_files}
COMPONENT_DEPENDENCIES
interp
opt
portfolio
realclosure

2
src/api/api_ast.cpp
View file

@ -195,7 +195,6 @@ 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_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));
@ -900,7 +899,6 @@ extern "C" {
case OP_NOT: return Z3_OP_NOT;
case OP_IMPLIES: return Z3_OP_IMPLIES;
case OP_OEQ: return Z3_OP_OEQ;
case OP_INTERP: return Z3_OP_INTERP;
case PR_UNDEF: return Z3_OP_PR_UNDEF;
case PR_TRUE: return Z3_OP_PR_TRUE;

1
src/api/dotnet/CMakeLists.txt
View file

@ -80,7 +80,6 @@ set(Z3_DOTNET_ASSEMBLY_SOURCES_IN_SRC_TREE
Global.cs
Goal.cs
IDecRefQueue.cs
InterpolationContext.cs
IntExpr.cs
IntNum.cs
IntSort.cs

161
src/api/dotnet/InterpolationContext.cs
View file

@ -1,161 +0,0 @@
/*++
Copyright (c) 2015 Microsoft Corporation
--*/
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)]
public class InterpolationContext : Context
{
/// <summary>
/// Constructor.
/// </summary>
public InterpolationContext() : base() { }
/// <summary>
/// Constructor.
/// </summary>
/// <remarks><seealso cref="Context"/></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>
public BoolExpr[] 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));
return seq.ToBoolExprArray();
}
/// <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>
public Z3_lbool ComputeInterpolant(Expr pat, Params p, out BoolExpr[] 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).ToBoolExprArray();
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, BoolExpr[] 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;
IntPtr n_err_str;
ASTVector _cnsts = new ASTVector(this);
ASTVector _theory = new ASTVector(this);
int r = Native.Z3_read_interpolation_problem(nCtx, _cnsts.NativeObject, ref num, out parents, filename, out n_err_str, _theory.NativeObject);
error = Marshal.PtrToStringAnsi(n_err_str);
cnsts = _cnsts.ToExprArray();
parents = new uint[num];
theory = _theory.ToExprArray();
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));
}
}
}

1
src/api/java/CMakeLists.txt
View file

@ -137,7 +137,6 @@ set(Z3_JAVA_JAR_SOURCE_FILES
GoalDecRefQueue.java
Goal.java
IDecRefQueue.java
InterpolationContext.java
IntExpr.java
IntNum.java
IntSort.java

210
src/api/java/InterpolationContext.java
View file

@ -1,210 +0,0 @@
/**
Copyright (c) 2012-2014 Microsoft Corporation
Module Name:
InterpolationContext.java
Abstract:
Author:
@author Christoph Wintersteiger (cwinter) 2012-03-15
Notes:
**/
package com.microsoft.z3;
import com.microsoft.z3.enumerations.Z3_lbool;
import java.util.Map;
/**
* The InterpolationContext is suitable for generation of interpolants.
*
* Remarks: For more information on interpolation please refer
* too the C/C++ API, which is well documented.
**/
public class InterpolationContext extends Context
{
/**
* Constructor.
**/
public static InterpolationContext mkContext()
{
long m_ctx;
synchronized(creation_lock) {
m_ctx = Native.mkInterpolationContext(0);
}
return new InterpolationContext(m_ctx);
}
/**
* Constructor.
*
*
* Remarks:
* @see Context#Context
**/
public static InterpolationContext mkContext(Map<String, String> settings)
{
long m_ctx;
synchronized(creation_lock) {
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);
}
return new InterpolationContext(m_ctx);
}
private InterpolationContext(long m_ctx) {
super(m_ctx);
}
/**
* Create an expression that marks a formula position for interpolation.
* @throws Z3Exception
**/
public BoolExpr MkInterpolant(BoolExpr a)
{
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.
* @throws Z3Exception
**/
public BoolExpr[] GetInterpolant(Expr pf, Expr pat, Params p)
{
checkContextMatch(pf);
checkContextMatch(pat);
checkContextMatch(p);
ASTVector seq = new ASTVector(this, Native.getInterpolant(nCtx(), pf.getNativeObject(), pat.getNativeObject(), p.getNativeObject()));
return seq.ToBoolExprArray();
}
public class ComputeInterpolantResult
{
public Z3_lbool status = Z3_lbool.Z3_L_UNDEF;
public BoolExpr[] interp = null;
public Model model = null;
};
/**
* 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.
* @throws Z3Exception
**/
public ComputeInterpolantResult ComputeInterpolant(Expr pat, Params p)
{
checkContextMatch(pat);
checkContextMatch(p);
ComputeInterpolantResult res = new ComputeInterpolantResult();
Native.LongPtr n_i = new Native.LongPtr();
Native.LongPtr n_m = new Native.LongPtr();
res.status = Z3_lbool.fromInt(Native.computeInterpolant(nCtx(), pat.getNativeObject(), p.getNativeObject(), n_i, n_m));
if (res.status == Z3_lbool.Z3_L_FALSE)
res.interp = (new ASTVector(this, n_i.value)).ToBoolExprArray();
if (res.status == Z3_lbool.Z3_L_TRUE)
res.model = new Model(this, n_m.value);
return res;
}
///
/// Return a string summarizing cumulative time used for interpolation.
///
/// Remarks: For more information on interpolation please refer
/// too the function Z3_interpolation_profile in the C/C++ API, which is
/// well documented.
public String InterpolationProfile()
{
return Native.interpolationProfile(nCtx());
}
public class CheckInterpolantResult
{
public int return_value = 0;
public String error = null;
}
///
/// Checks the correctness of an interpolant.
///
/// Remarks: For more information on interpolation please refer
/// too the function Z3_check_interpolant in the C/C++ API, which is
/// well documented.
public CheckInterpolantResult CheckInterpolant(Expr[] cnsts, int[] parents, BoolExpr[] interps, String error, Expr[] theory)
{
CheckInterpolantResult res = new CheckInterpolantResult();
Native.StringPtr n_err_str = new Native.StringPtr();
res.return_value = Native.checkInterpolant(nCtx(),
cnsts.length,
Expr.arrayToNative(cnsts),
parents,
Expr.arrayToNative(interps),
n_err_str,
theory.length,
Expr.arrayToNative(theory));
res.error = n_err_str.value;
return res;
}
public class ReadInterpolationProblemResult
{
public int return_value = 0;
public Expr[] cnsts;
public int[] parents;
public String error;
public Expr[] theory;
};
///
/// Reads an interpolation problem from a file.
///
/// Remarks: For more information on interpolation please refer
/// too the function Z3_read_interpolation_problem in the C/C++ API, which is
/// well documented.
public ReadInterpolationProblemResult ReadInterpolationProblem(String filename)
{
ReadInterpolationProblemResult res = new ReadInterpolationProblemResult();
Native.UIntArrayPtr n_parents = new Native.UIntArrayPtr();
ASTVector _cnsts = new ASTVector(this);
ASTVector _theory = new ASTVector(this);
Native.StringPtr n_err_str = new Native.StringPtr();
Native.IntPtr n_num = new Native.IntPtr();
res.return_value = Native.readInterpolationProblem(nCtx(), _cnsts.getNativeObject(), n_num,
n_parents, filename, n_err_str, _theory.getNativeObject());
res.error = n_err_str.value;
res.theory = _theory.ToExprArray();
res.cnsts = _cnsts.ToExprArray();
int num = n_num.value;
res.parents = new int[num];
for (int i = 0; i < num; i++) {
res.parents[i] = n_parents.value[i];
}
return res;
}
///
/// Writes an interpolation problem to a file.
///
/// Remarks: For more information on interpolation please refer
/// too the function Z3_write_interpolation_problem in the C/C++ API, which is
/// well documented.
public void WriteInterpolationProblem(String filename, Expr[] cnsts, int[] parents, String error, Expr[] theory)
{
Native.writeInterpolationProblem(nCtx(), cnsts.length, Expr.arrayToNative(cnsts), parents, filename, theory.length, Expr.arrayToNative(theory));
}
}

1
src/api/z3.h
View file

@ -32,7 +32,6 @@ Notes:
#include "z3_rcf.h"
#include "z3_fixedpoint.h"
#include "z3_optimization.h"
#include "z3_interp.h"
#include "z3_fpa.h"
#include "z3_spacer.h"
#endif

3
src/api/z3_api.h
View file

@ -212,8 +212,6 @@ typedef enum
- Z3_OP_OEQ Binary equivalence modulo namings. This binary predicate is used in proof terms.
It captures equisatisfiability and equivalence modulo renamings.
- Z3_OP_INTERP Marks a sub-formula for interpolation.
- Z3_OP_ANUM Arithmetic numeral.
- Z3_OP_AGNUM Arithmetic algebraic numeral. Algebraic numbers are used to represent irrational numbers in Z3.
@ -991,7 +989,6 @@ typedef enum {
Z3_OP_NOT,
Z3_OP_IMPLIES,
Z3_OP_OEQ,
Z3_OP_INTERP,
// Arithmetic
Z3_OP_ANUM = 0x200,

283
src/api/z3_interp.h
View file

@ -1,283 +0,0 @@
/*++
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 facilities */
/*@{*/
/**
\brief 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(Z3_context c, 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(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 interpolation 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
\c 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(Z3_context c, Z3_ast pf, Z3_ast pat, 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(Z3_context c,
Z3_ast pat,
Z3_params p,
Z3_ast_vector *interp,
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(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 associated to node v. The last formula in the
file is the root vertex, and is represented by the predicate "false".
A solution to a tree interpolation problem can be thought of as a
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), _in(AST_VECTOR), _out(UINT), _out_managed_array(2, UINT), _in(STRING), _out(STRING), _in(AST_VECTOR)))
*/
int Z3_API Z3_read_interpolation_problem(Z3_context ctx,
Z3_ast_vector cnsts,
unsigned* num,
unsigned* parents[],
Z3_string filename,
Z3_string_ptr error,
Z3_ast_vector 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(Z3_context ctx,
unsigned num,
Z3_ast cnsts[],
unsigned parents[],
Z3_ast *interps,
Z3_string_ptr error,
unsigned 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(Z3_context ctx,
unsigned num,
Z3_ast cnsts[],
unsigned parents[],
Z3_string filename,
unsigned num_theory,
Z3_ast theory[]);
/*@}*/
/*@}*/
#ifdef __cplusplus
}
#endif // __cplusplus
#endif

7
src/ast/ast.cpp
View file

@ -646,7 +646,6 @@ basic_decl_plugin::basic_decl_plugin():
m_iff_decl(nullptr),
m_xor_decl(nullptr),
m_not_decl(nullptr),
m_interp_decl(nullptr),
m_implies_decl(nullptr),
m_proof_sort(nullptr),
@ -865,7 +864,6 @@ void basic_decl_plugin::set_manager(ast_manager * m, family_id id) {
m_iff_decl = mk_bool_op_decl("iff", OP_IFF, 2, false, true, false, false, true);
m_xor_decl = mk_bool_op_decl("xor", OP_XOR, 2, true, true);
m_not_decl = mk_bool_op_decl("not", OP_NOT, 1);
m_interp_decl = mk_bool_op_decl("interp", OP_INTERP, 1);
m_implies_decl = mk_implies_decl();
m_proof_sort = m->mk_sort(symbol("Proof"), sort_info(id, PROOF_SORT));
@ -890,7 +888,6 @@ void basic_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol co
op_names.push_back(builtin_name("or", OP_OR));
op_names.push_back(builtin_name("xor", OP_XOR));
op_names.push_back(builtin_name("not", OP_NOT));
op_names.push_back(builtin_name("interp", OP_INTERP));
op_names.push_back(builtin_name("=>", OP_IMPLIES));
if (logic == symbol::null) {
// user friendly aliases
@ -902,7 +899,6 @@ void basic_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol co
op_names.push_back(builtin_name("||", OP_OR));
op_names.push_back(builtin_name("equals", OP_EQ));
op_names.push_back(builtin_name("equiv", OP_IFF));
op_names.push_back(builtin_name("@@", OP_INTERP));
}
}
@ -923,7 +919,6 @@ void basic_decl_plugin::finalize() {
DEC_REF(m_and_decl);
DEC_REF(m_or_decl);
DEC_REF(m_not_decl);
DEC_REF(m_interp_decl);
DEC_REF(m_iff_decl);
DEC_REF(m_xor_decl);
DEC_REF(m_implies_decl);
@ -1056,7 +1051,6 @@ func_decl * basic_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
case OP_AND: return m_and_decl;
case OP_OR: return m_or_decl;
case OP_NOT: return m_not_decl;
case OP_INTERP: return m_interp_decl;
case OP_IFF: return m_iff_decl;
case OP_IMPLIES: return m_implies_decl;
case OP_XOR: return m_xor_decl;
@ -1099,7 +1093,6 @@ func_decl * basic_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
case OP_AND: return m_and_decl;
case OP_OR: return m_or_decl;
case OP_NOT: return m_not_decl;
case OP_INTERP: return m_interp_decl;
case OP_IFF: return m_iff_decl;
case OP_IMPLIES: return m_implies_decl;
case OP_XOR: return m_xor_decl;

4
src/ast/ast.h
View file

@ -1041,7 +1041,7 @@ enum basic_sort_kind {
};
enum basic_op_kind {
OP_TRUE, OP_FALSE, OP_EQ, OP_DISTINCT, OP_ITE, OP_AND, OP_OR, OP_IFF, OP_XOR, OP_NOT, OP_IMPLIES, OP_OEQ, OP_INTERP, LAST_BASIC_OP,
OP_TRUE, OP_FALSE, OP_EQ, OP_DISTINCT, OP_ITE, OP_AND, OP_OR, OP_IFF, OP_XOR, OP_NOT, OP_IMPLIES, OP_OEQ, LAST_BASIC_OP,
PR_UNDEF, PR_TRUE, PR_ASSERTED, PR_GOAL, PR_MODUS_PONENS, PR_REFLEXIVITY, PR_SYMMETRY, PR_TRANSITIVITY, PR_TRANSITIVITY_STAR, PR_MONOTONICITY, PR_QUANT_INTRO,
PR_DISTRIBUTIVITY, PR_AND_ELIM, PR_NOT_OR_ELIM, PR_REWRITE, PR_REWRITE_STAR, PR_PULL_QUANT,
@ -1063,7 +1063,6 @@ protected:
func_decl * m_iff_decl;
func_decl * m_xor_decl;
func_decl * m_not_decl;
func_decl * m_interp_decl;
func_decl * m_implies_decl;
ptr_vector<func_decl> m_eq_decls; // cached eqs
ptr_vector<func_decl> m_ite_decls; // cached ites
@ -2054,7 +2053,6 @@ public:
app * mk_true() const { return m_true; }
app * mk_false() const { return m_false; }
app * mk_bool_val(bool b) { return b?m_true:m_false; }
app * mk_interp(expr * arg) { return mk_app(m_basic_family_id, OP_INTERP, arg); }
func_decl* mk_and_decl() {

2
src/cmd_context/CMakeLists.txt
View file

@ -8,14 +8,12 @@ z3_add_component(cmd_context
context_params.cpp
echo_tactic.cpp
eval_cmd.cpp
interpolant_cmds.cpp
parametric_cmd.cpp
pdecl.cpp
simplify_cmd.cpp
tactic_cmds.cpp
tactic_manager.cpp
COMPONENT_DEPENDENCIES
interp
rewriter
solver
EXTRA_REGISTER_MODULE_HEADERS

2
src/cmd_context/cmd_context.cpp
View file

@ -46,7 +46,6 @@ Notes:
#include "tactic/generic_model_converter.h"
#include "solver/smt_logics.h"
#include "cmd_context/basic_cmds.h"
#include "cmd_context/interpolant_cmds.h"
#include "cmd_context/cmd_context.h"
func_decls::func_decls(ast_manager & m, func_decl * f):
@ -484,7 +483,6 @@ cmd_context::cmd_context(bool main_ctx, ast_manager * m, symbol const & l):
install_basic_cmds(*this);
install_ext_basic_cmds(*this);
install_core_tactic_cmds(*this);
install_interpolant_cmds(*this);
SASSERT(m != 0 || !has_manager());
if (m_main_ctx) {
set_verbose_stream(diagnostic_stream());

263
src/cmd_context/interpolant_cmds.cpp
View file

@ -1,263 +0,0 @@
/*++
Copyright (c) 2013 Microsoft Corporation
Module Name:
interpolant_cmds.cpp
Abstract:
Commands for interpolation.
Author:
Leonardo (leonardo) 2011-12-23
Notes:
--*/
#include<sstream>
#include "cmd_context/cmd_context.h"
#include "cmd_context/cmd_util.h"
#include "util/scoped_timer.h"
#include "util/scoped_ctrl_c.h"
#include "util/cancel_eh.h"
#include "ast/ast_pp.h"
#include "ast/ast_smt_pp.h"
#include "ast/ast_smt2_pp.h"
#include "cmd_context/parametric_cmd.h"
#include "util/mpq.h"
#include "ast/expr2var.h"
#include "ast/pp.h"
#include "interp/iz3interp.h"
#include "interp/iz3checker.h"
#include "interp/iz3profiling.h"
#include "interp/interp_params.hpp"
#include "ast/scoped_proof.h"
static void show_interpolant_and_maybe_check(cmd_context & ctx,
ptr_vector<ast> &cnsts,
expr *t,
ptr_vector<ast> &interps,
params_ref &m_params,
bool check)
{
if (m_params.get_bool("som", false))
m_params.set_bool("flat", true);
th_rewriter s(ctx.m(), m_params);
ctx.regular_stream() << "(interpolants";
for(unsigned i = 0; i < interps.size(); i++){
expr_ref r(ctx.m());
proof_ref pr(ctx.m());
s(to_expr(interps[i]),r,pr);
ctx.regular_stream() << "\n " << r;
}
ctx.regular_stream() << ")\n";
s.cleanup();
// verify, for the paranoid...
if(check || interp_params(m_params).check()){
std::ostringstream err;
ast_manager &_m = ctx.m();
// need a solver -- make one here FIXME is this right?
bool proofs_enabled, models_enabled, unsat_core_enabled;
params_ref p;
ctx.params().get_solver_params(_m, p, proofs_enabled, models_enabled, unsat_core_enabled);
scoped_ptr<solver> sp = (ctx.get_solver_factory())(_m, p, false, true, false, ctx.get_logic());
if(iz3check(_m,sp.get(),err,cnsts,t,interps))
ctx.regular_stream() << "correct\n";
else
ctx.regular_stream() << "incorrect: " << err.str().c_str() << "\n";
}
for(unsigned i = 0; i < interps.size(); i++){
ctx.m().dec_ref(interps[i]);
}
interp_params itp_params(m_params);
if(itp_params.profile())
profiling::print(ctx.regular_stream());
}
static void check_can_interpolate(cmd_context & ctx){
if (!ctx.produce_interpolants())
throw cmd_exception("interpolation is not enabled, use command (set-option :produce-interpolants true)");
}
static void get_interpolant_and_maybe_check(cmd_context & ctx, expr * t, params_ref &m_params, bool check) {
check_can_interpolate(ctx);
// get the proof, if there is one
if (!ctx.has_manager() ||
ctx.cs_state() != cmd_context::css_unsat)
throw cmd_exception("proof is not available");
expr_ref pr(ctx.m());
pr = ctx.get_check_sat_result()->get_proof();
if (pr == 0)
throw cmd_exception("proof is not available");
// get the assertions from the context
ptr_vector<expr>::const_iterator it = ctx.begin_assertions();
ptr_vector<expr>::const_iterator end = ctx.end_assertions();
ptr_vector<ast> cnsts((unsigned)(end - it));
for (int i = 0; it != end; ++it, ++i)
cnsts[i] = *it;
// compute an interpolant
ptr_vector<ast> interps;
try {
iz3interpolate(ctx.m(),pr.get(),cnsts,t,interps,nullptr);
}
catch (iz3_bad_tree &) {
throw cmd_exception("interpolation pattern contains non-asserted formula");
}
catch (iz3_incompleteness &) {
throw cmd_exception("incompleteness in interpolator");
}
show_interpolant_and_maybe_check(ctx, cnsts, t, interps, m_params, check);
}
static void get_interpolant(cmd_context & ctx, expr * t, params_ref &m_params) {
get_interpolant_and_maybe_check(ctx,t,m_params,false);
}
#if 0
static void get_and_check_interpolant(cmd_context & ctx, params_ref &m_params, expr * t) {
get_interpolant_and_maybe_check(ctx,t,m_params,true);
}
#endif
static void compute_interpolant_and_maybe_check(cmd_context & ctx, expr * t, params_ref &m_params, bool check){
// create a fresh solver suitable for interpolation
bool proofs_enabled, models_enabled, unsat_core_enabled;
params_ref p;
ast_manager &_m = ctx.m();
// TODO: the following is a HACK to enable proofs in the old smt solver
// When we stop using that solver, this hack can be removed
scoped_proof_mode spm(_m,PGM_ENABLED);
ctx.params().get_solver_params(_m, p, proofs_enabled, models_enabled, unsat_core_enabled);
p.set_bool("proof", true);
scoped_ptr<solver> sp = (ctx.get_interpolating_solver_factory())(_m, p, true, models_enabled, false, ctx.get_logic());
ptr_vector<ast> cnsts;
ptr_vector<ast> interps;
model_ref m;
// compute an interpolant
lbool res;
try {
res = iz3interpolate(_m, *sp.get(), t, cnsts, interps, m, nullptr);
}
catch (iz3_incompleteness &) {
throw cmd_exception("incompleteness in interpolator");
}
switch(res){
case l_false:
ctx.regular_stream() << "unsat\n";
show_interpolant_and_maybe_check(ctx, cnsts, t, interps, m_params, check);
break;
case l_true:
ctx.regular_stream() << "sat\n";
// TODO: how to return the model to the context, if it exists?
break;
case l_undef:
ctx.regular_stream() << "unknown\n";
// TODO: how to return the model to the context, if it exists?
break;
}
for(unsigned i = 0; i < cnsts.size(); i++)
ctx.m().dec_ref(cnsts[i]);
}
static expr *make_tree(cmd_context & ctx, const ptr_vector<expr> &exprs){
if(exprs.size() == 0)
throw cmd_exception("not enough arguments");
expr *foo = exprs[0];
for(unsigned i = 1; i < exprs.size(); i++){
foo = ctx.m().mk_and(ctx.m().mk_interp(foo),exprs[i]);
}
return foo;
}
static void get_interpolant(cmd_context & ctx, const ptr_vector<expr> &exprs, params_ref &m_params) {
expr_ref foo(make_tree(ctx, exprs),ctx.m());
get_interpolant(ctx,foo.get(),m_params);
}
static void compute_interpolant(cmd_context & ctx, const ptr_vector<expr> &exprs, params_ref &m_params) {
expr_ref foo(make_tree(ctx, exprs),ctx.m());
compute_interpolant_and_maybe_check(ctx,foo.get(),m_params,false);
}
// UNARY_CMD(get_interpolant_cmd, "get-interpolant", "<fmla>", "get interpolant for marked positions in fmla", CPK_EXPR, expr *, get_interpolant(ctx, arg););
// UNARY_CMD(get_and_check_interpolant_cmd, "get-and-check-interpolant", "<fmla>", "get and check interpolant for marked positions in fmla", CPK_EXPR, expr *, get_and_check_interpolant(ctx, arg););
class get_interpolant_cmd : public parametric_cmd {
protected:
ptr_vector<expr> m_targets;
public:
get_interpolant_cmd(char const * name = "get-interpolant"):parametric_cmd(name) {}
char const * get_usage() const override { return "<fmla>+"; }
char const * get_main_descr() const override {
return "get interpolant for formulas";
}
void init_pdescrs(cmd_context & ctx, param_descrs & p) override {
}
void prepare(cmd_context & ctx) override {
parametric_cmd::prepare(ctx);
m_targets.resize(0);
}
cmd_arg_kind next_arg_kind(cmd_context & ctx) const override {
return CPK_EXPR;
}
void set_next_arg(cmd_context & ctx, expr * arg) override {
m_targets.push_back(arg);
}
void execute(cmd_context & ctx) override {
get_interpolant(ctx,m_targets,m_params);
}
};
class compute_interpolant_cmd : public get_interpolant_cmd {
public:
compute_interpolant_cmd(char const * name = "compute-interpolant"):get_interpolant_cmd(name) {}
void execute(cmd_context & ctx) override {
compute_interpolant(ctx,m_targets,m_params);
}
};
void install_interpolant_cmds(cmd_context & ctx) {
ctx.insert(alloc(get_interpolant_cmd));
ctx.insert(alloc(compute_interpolant_cmd));
// ctx.insert(alloc(get_and_check_interpolant_cmd));
}

24
src/cmd_context/interpolant_cmds.h
View file

@ -1,24 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
interpolant_cmds.h
Abstract:
Commands for interpolation.
Author:
Leonardo (leonardo) 2011-12-23
Notes:
--*/
#ifndef INTERPOLANT_CMDS_H_
#define INTERPOLANT_CMDS_H_
class cmd_context;
void install_interpolant_cmds(cmd_context & ctx);
#endif

11
src/duality/CMakeLists.txt
View file

@ -1,11 +0,0 @@
z3_add_component(duality
SOURCES
duality_profiling.cpp
duality_rpfp.cpp
duality_solver.cpp
duality_wrapper.cpp
COMPONENT_DEPENDENCIES
interp
qe
smt
)

1365
src/duality/duality.h
View file

File diff suppressed because it is too large Load diff

144
src/duality/duality_profiling.cpp
View file

@ -1,144 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
duality_profiling.cpp
Abstract:
collection performance information for duality
Author:
Ken McMillan (kenmcmil)
Revision History:
--*/
#include <map>
#include <iostream>
#include <string>
#include <string.h>
#include <stdlib.h>
#ifdef _WINDOWS
#pragma warning(disable:4996)
#pragma warning(disable:4800)
#pragma warning(disable:4267)
#endif
#include "duality/duality_wrapper.h"
#include "interp/iz3profiling.h"
namespace Duality {
void show_time(){
output_time(std::cout,current_time());
std::cout << "\n";
}
typedef std::map<const char*, struct node> nmap;
struct node {
std::string name;
clock_t time;
clock_t start_time;
nmap sub;
struct node *parent;
node();
} top;
node::node(){
time = 0;
parent = nullptr;
}
struct node *current;
struct init {
init(){
top.name = "TOTAL";
current = &top;
}
} initializer;
struct time_entry {
clock_t t;
time_entry(){t = 0;};
void add(clock_t incr){t += incr;}
};
struct ltstr
{
bool operator()(const char* s1, const char* s2) const
{
return strcmp(s1, s2) < 0;
}
};
typedef std::map<const char*, time_entry, ltstr> tmap;
static std::ostream *pfs;
void print_node(node &top, int indent, tmap &totals){
for(int i = 0; i < indent; i++) (*pfs) << " ";
(*pfs) << top.name;
int dots = 70 - 2 * indent - top.name.size();
for(int i = 0; i <dots; i++) (*pfs) << ".";
output_time(*pfs, top.time);
(*pfs) << std::endl;
if(indent != 0)totals[top.name.c_str()].add(top.time);
for(nmap::iterator it = top.sub.begin(); it != top.sub.end(); it++)
print_node(it->second,indent+1,totals);
}
void print_profile(std::ostream &os) {
pfs = &os;
top.time = 0;
for(nmap::iterator it = top.sub.begin(); it != top.sub.end(); it++)
top.time += it->second.time;
tmap totals;
print_node(top,0,totals);
(*pfs) << "TOTALS:" << std::endl;
for(tmap::iterator it = totals.begin(); it != totals.end(); it++){
(*pfs) << (it->first) << " ";
output_time(*pfs, it->second.t);
(*pfs) << std::endl;
}
profiling::print(os); // print the interpolation stats
}
void timer_start(const char *name){
node &child = current->sub[name];
if(child.name.empty()){ // a new node
child.parent = current;
child.name = name;
}
child.start_time = current_time();
current = &child;
}
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;
}
}

38
src/duality/duality_profiling.h
View file

@ -1,38 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
duality_profiling.h
Abstract:
collection performance information for duality
Author:
Ken McMillan (kenmcmil)
Revision History:
--*/
#ifndef DUALITYPROFILING_H
#define DUALITYPROFILING_H
#include <ostream>
namespace Duality {
/** Start a timer with given name */
void timer_start(const char *);
/** Stop a timer with given name */
void timer_stop(const char *);
/** Print out timings */
void print_profile(std::ostream &s);
/** Show the current time. */
void show_time();
}
#endif

4250
src/duality/duality_rpfp.cpp
View file

File diff suppressed because it is too large Load diff

3601
src/duality/duality_solver.cpp
View file

File diff suppressed because it is too large Load diff

744
src/duality/duality_wrapper.cpp
View file

@ -1,744 +0,0 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
wrapper.cpp
Abstract:
wrap various objects in the style expected by duality
Author:
Ken McMillan (kenmcmil)
Revision History:
--*/
#ifdef _WINDOWS
#pragma warning(disable:4996)
#pragma warning(disable:4800)
#pragma warning(disable:4267)
#pragma warning(disable:4101)
#endif
#include "duality/duality_wrapper.h"
#include <iostream>
#include "smt/smt_solver.h"
#include "interp/iz3interp.h"
#include "util/statistics.h"
#include "ast/expr_abstract.h"
#include "util/stopwatch.h"
#include "model/model_smt2_pp.h"
#include "qe/qe_lite.h"
namespace Duality {
solver::solver(Duality::context& c, bool _extensional, bool models) : object(c), the_model(c) {
params_ref p;
p.set_bool("proof", true); // this is currently useless
if(models)
p.set_bool("model", true);
p.set_bool("unsat_core", true);
bool mbqi = c.get_config().get().get_bool("mbqi",true);
p.set_bool("mbqi",mbqi); // just to test
p.set_str("mbqi.id","itp"); // use mbqi for quantifiers in interpolants
p.set_uint("mbqi.max_iterations",1); // use mbqi for quantifiers in interpolants
extensional = mbqi && (true || _extensional);
if(extensional)
p.set_bool("array.extensional",true);
scoped_ptr<solver_factory> sf = mk_smt_solver_factory();
m_solver = (*sf)(m(), p, true, true, true, ::symbol::null);
m_solver->updt_params(p); // why do we have to do this?
canceled = false;
m_mode = m().proof_mode();
}
expr context::constant(const std::string &name, const sort &ty){
symbol s = str_symbol(name.c_str());
return cook(m().mk_const(m().mk_const_decl(s, ty)));
}
expr context::make(decl_kind op, int n, ::expr **args){
switch(op) {
case True: return mki(m_basic_fid,OP_TRUE,n,args);
case False: return mki(m_basic_fid,OP_FALSE,n,args);
case Equal: return mki(m_basic_fid,OP_EQ,n,args);
case Distinct: return mki(m_basic_fid,OP_DISTINCT,n,args);
case Ite: return mki(m_basic_fid,OP_ITE,n,args);
case And: return mki(m_basic_fid,OP_AND,n,args);
case Or: return mki(m_basic_fid,OP_OR,n,args);
case Iff: return mki(m_basic_fid,OP_IFF,n,args);
case Xor: return mki(m_basic_fid,OP_XOR,n,args);
case Not: return mki(m_basic_fid,OP_NOT,n,args);
case Implies: return mki(m_basic_fid,OP_IMPLIES,n,args);
case Oeq: return mki(m_basic_fid,OP_OEQ,n,args);
case Interp: return mki(m_basic_fid,OP_INTERP,n,args);
case Leq: return mki(m_arith_fid,OP_LE,n,args);
case Geq: return mki(m_arith_fid,OP_GE,n,args);
case Lt: return mki(m_arith_fid,OP_LT,n,args);
case Gt: return mki(m_arith_fid,OP_GT,n,args);
case Plus: return mki(m_arith_fid,OP_ADD,n,args);
case Sub: return mki(m_arith_fid,OP_SUB,n,args);
case Uminus: return mki(m_arith_fid,OP_UMINUS,n,args);
case Times: return mki(m_arith_fid,OP_MUL,n,args);
case Div: return mki(m_arith_fid,OP_DIV,n,args);
case Idiv: return mki(m_arith_fid,OP_IDIV,n,args);
case Rem: return mki(m_arith_fid,OP_REM,n,args);
case Mod: return mki(m_arith_fid,OP_MOD,n,args);
case Power: return mki(m_arith_fid,OP_POWER,n,args);
case ToReal: return mki(m_arith_fid,OP_TO_REAL,n,args);
case ToInt: return mki(m_arith_fid,OP_TO_INT,n,args);
case IsInt: return mki(m_arith_fid,OP_IS_INT,n,args);
case Store: return mki(m_array_fid,OP_STORE,n,args);
case Select: return mki(m_array_fid,OP_SELECT,n,args);
case ConstArray: return mki(m_array_fid,OP_CONST_ARRAY,n,args);
case ArrayDefault: return mki(m_array_fid,OP_ARRAY_DEFAULT,n,args);
case ArrayMap: return mki(m_array_fid,OP_ARRAY_MAP,n,args);
case SetUnion: return mki(m_array_fid,OP_SET_UNION,n,args);
case SetIntersect: return mki(m_array_fid,OP_SET_INTERSECT,n,args);
case SetDifference: return mki(m_array_fid,OP_SET_DIFFERENCE,n,args);
case SetComplement: return mki(m_array_fid,OP_SET_COMPLEMENT,n,args);
case SetSubSet: return mki(m_array_fid,OP_SET_SUBSET,n,args);
case AsArray: return mki(m_array_fid,OP_AS_ARRAY,n,args);
default:
assert(0);
return expr(*this);
}
}
expr context::mki(family_id fid, ::decl_kind dk, int n, ::expr **args){
return cook(m().mk_app(fid, dk, 0, nullptr, n, (::expr **)args));
}
expr context::make(decl_kind op, const std::vector<expr> &args){
static std::vector< ::expr*> a(10);
if(a.size() < args.size())
a.resize(args.size());
for(unsigned i = 0; i < args.size(); i++)
a[i] = to_expr(args[i].raw());
return make(op,args.size(), args.size() ? VEC2PTR(a) : nullptr);
}
expr context::make(decl_kind op){
return make(op,0,nullptr);
}
expr context::make(decl_kind op, const expr &arg0){
::expr *a = to_expr(arg0.raw());
return make(op,1,&a);
}
expr context::make(decl_kind op, const expr &arg0, const expr &arg1){
::expr *args[2];
args[0] = to_expr(arg0.raw());
args[1] = to_expr(arg1.raw());
return make(op,2,args);
}
expr context::make(decl_kind op, const expr &arg0, const expr &arg1, const expr &arg2){
::expr *args[3];
args[0] = to_expr(arg0.raw());
args[1] = to_expr(arg1.raw());
args[2] = to_expr(arg2.raw());
return make(op,3,args);
}
expr context::make_quant(decl_kind op, const std::vector<expr> &bvs, const expr &body){
if(bvs.size() == 0) return body;
std::vector< ::expr *> foo(bvs.size());
std::vector< ::symbol> names;
std::vector< ::sort *> types;
std::vector< ::expr *> bound_asts;
unsigned num_bound = bvs.size();
for (unsigned i = 0; i < num_bound; ++i) {
app* a = to_app(bvs[i].raw());
::symbol s(to_app(a)->get_decl()->get_name());
names.push_back(s);
types.push_back(m().get_sort(a));
bound_asts.push_back(a);
}
expr_ref abs_body(m());
expr_abstract(m(), 0, num_bound, VEC2PTR(bound_asts), to_expr(body.raw()), abs_body);
expr_ref result(m());
result = m().mk_quantifier(
op == Forall,
names.size(), VEC2PTR(types), VEC2PTR(names), abs_body.get(),
0,
::symbol(),
::symbol(),
0, nullptr,
0, nullptr
);
return cook(result.get());
}
expr context::make_quant(decl_kind op, const std::vector<sort> &_sorts, const std::vector<symbol> &_names, const expr &body){
if(_sorts.size() == 0) return body;
std::vector< ::symbol> names;
std::vector< ::sort *> types;
std::vector< ::expr *> bound_asts;
unsigned num_bound = _sorts.size();
for (unsigned i = 0; i < num_bound; ++i) {
names.push_back(_names[i]);
types.push_back(to_sort(_sorts[i].raw()));
}
expr_ref result(m());
result = m().mk_quantifier(
op == Forall,
names.size(), VEC2PTR(types), VEC2PTR(names), to_expr(body.raw()),
0,
::symbol(),
::symbol(),
0, nullptr,
0, nullptr
);
return cook(result.get());
}
decl_kind func_decl::get_decl_kind() const {
return ctx().get_decl_kind(*this);
}
decl_kind context::get_decl_kind(const func_decl &t){
::func_decl *d = to_func_decl(t.raw());
if (null_family_id == d->get_family_id())
return Uninterpreted;
// return (opr)d->get_decl_kind();
if (m_basic_fid == d->get_family_id()) {
switch(d->get_decl_kind()) {
case OP_TRUE: return True;
case OP_FALSE: return False;
case OP_EQ: return Equal;
case OP_DISTINCT: return Distinct;
case OP_ITE: return Ite;
case OP_AND: return And;
case OP_OR: return Or;
case OP_IFF: return Iff;
case OP_XOR: return Xor;
case OP_NOT: return Not;
case OP_IMPLIES: return Implies;
case OP_OEQ: return Oeq;
case OP_INTERP: return Interp;
default:
return OtherBasic;
}
}
if (m_arith_fid == d->get_family_id()) {
switch(d->get_decl_kind()) {
case OP_LE: return Leq;
case OP_GE: return Geq;
case OP_LT: return Lt;
case OP_GT: return Gt;
case OP_ADD: return Plus;
case OP_SUB: return Sub;
case OP_UMINUS: return Uminus;
case OP_MUL: return Times;
case OP_DIV: return Div;
case OP_IDIV: return Idiv;
case OP_REM: return Rem;
case OP_MOD: return Mod;
case OP_POWER: return Power;
case OP_TO_REAL: return ToReal;
case OP_TO_INT: return ToInt;
case OP_IS_INT: return IsInt;
default:
return OtherArith;
}
}
if (m_array_fid == d->get_family_id()) {
switch(d->get_decl_kind()) {
case OP_STORE: return Store;
case OP_SELECT: return Select;
case OP_CONST_ARRAY: return ConstArray;
case OP_ARRAY_DEFAULT: return ArrayDefault;
case OP_ARRAY_MAP: return ArrayMap;
case OP_SET_UNION: return SetUnion;
case OP_SET_INTERSECT: return SetIntersect;
case OP_SET_DIFFERENCE: return SetDifference;
case OP_SET_COMPLEMENT: return SetComplement;
case OP_SET_SUBSET: return SetSubSet;
case OP_AS_ARRAY: return AsArray;
default:
return OtherArray;
}
}
return Other;
}
sort_kind context::get_sort_kind(const sort &s){
family_id fid = to_sort(s.raw())->get_family_id();
::decl_kind k = to_sort(s.raw())->get_decl_kind();
if (m().is_uninterp(to_sort(s.raw()))) {
return UninterpretedSort;
}
else if (fid == m_basic_fid && k == BOOL_SORT) {
return BoolSort;
}
else if (fid == m_arith_fid && k == INT_SORT) {
return IntSort;
}
else if (fid == m_arith_fid && k == REAL_SORT) {
return RealSort;
}
else if (fid == m_array_fid && k == ARRAY_SORT) {
return ArraySort;
}
else {
return UnknownSort;
}
}
expr func_decl::operator()(unsigned n, expr const * args) const {
std::vector< ::expr *> _args(n);
for(unsigned i = 0; i < n; i++)
_args[i] = to_expr(args[i].raw());
return ctx().cook(m().mk_app(to_func_decl(raw()),n,VEC2PTR(_args)));
}
int solver::get_num_decisions(){
::statistics st;
m_solver->collect_statistics(st);
std::ostringstream ss;
st.display(ss);
std::string stats = ss.str();
int pos = stats.find("decisions:");
if(pos < 0) return 0; // for some reason, decisions are not reported if there are none
pos += 10;
int end = stats.find('\n',pos);
std::string val = stats.substr(pos,end-pos);
return atoi(val.c_str());
}
void context::print_expr(std::ostream &s, const ast &e){
s << mk_pp(e.raw(), m());
}
expr expr::simplify(const params &_p) const {
::expr * a = to_expr(raw());
params_ref p = _p.get();
th_rewriter m_rw(m(), p);
expr_ref result(m());
m_rw(a, result);
return ctx().cook(result);
}
expr expr::simplify() const {
params p;
return simplify(p);
}
expr context::make_var(int idx, const sort &s){
::sort * a = to_sort(s.raw());
return cook(m().mk_var(idx,a));
}
expr expr::qe_lite() const {
::qe_lite qe(m(), params_ref());
expr_ref result(to_expr(raw()),m());
proof_ref pf(m());
qe(result,pf);
return ctx().cook(result);
}
expr expr::qe_lite(const std::set<int> &idxs, bool index_of_bound) const {
::qe_lite qe(m(), params_ref());
expr_ref result(to_expr(raw()),m());
proof_ref pf(m());
uint_set uis;
for(std::set<int>::const_iterator it=idxs.begin(), en = idxs.end(); it != en; ++it)
uis.insert(*it);
qe(uis,index_of_bound,result);
return ctx().cook(result);
}
expr clone_quantifier(const expr &q, const expr &b){
return q.ctx().cook(q.m().update_quantifier(to_quantifier(q.raw()), to_expr(b.raw())));
}
expr clone_quantifier(const expr &q, const expr &b, const std::vector<expr> &patterns){
quantifier *thing = to_quantifier(q.raw());
bool is_forall = thing->is_forall();
unsigned num_patterns = patterns.size();
std::vector< ::expr *> _patterns(num_patterns);
for(unsigned i = 0; i < num_patterns; i++)
_patterns[i] = to_expr(patterns[i].raw());
return q.ctx().cook(q.m().update_quantifier(thing, is_forall, num_patterns, VEC2PTR(_patterns), to_expr(b.raw())));
}
expr clone_quantifier(decl_kind dk, const expr &q, const expr &b){
quantifier *thing = to_quantifier(q.raw());
bool is_forall = dk == Forall;
return q.ctx().cook(q.m().update_quantifier(thing, is_forall, to_expr(b.raw())));
}
void expr::get_patterns(std::vector<expr> &pats) const {
quantifier *thing = to_quantifier(raw());
unsigned num_patterns = thing->get_num_patterns();
:: expr * const *it = thing->get_patterns();
pats.resize(num_patterns);
for(unsigned i = 0; i < num_patterns; i++)
pats[i] = expr(ctx(),it[i]);
}
unsigned func_decl::arity() const {
return (to_func_decl(raw())->get_arity());
}
sort func_decl::domain(unsigned i) const {
return sort(ctx(),(to_func_decl(raw())->get_domain(i)));
}
sort func_decl::range() const {
return sort(ctx(),(to_func_decl(raw())->get_range()));
}
func_decl context::fresh_func_decl(char const * prefix, const std::vector<sort> &domain, sort const & range){
std::vector < ::sort * > _domain(domain.size());
for(unsigned i = 0; i < domain.size(); i++)
_domain[i] = to_sort(domain[i].raw());
::func_decl* d = m().mk_fresh_func_decl(prefix,
_domain.size(),
VEC2PTR(_domain),
to_sort(range.raw()));
return func_decl(*this,d);
}
func_decl context::fresh_func_decl(char const * prefix, sort const & range){
::func_decl* d = m().mk_fresh_func_decl(prefix,
0,
nullptr,
to_sort(range.raw()));
return func_decl(*this,d);
}
#if 0
lbool interpolating_solver::interpolate(
const std::vector<expr> &assumptions,
std::vector<expr> &interpolants,
model &model,
Z3_literals &labels,
bool incremental)
{
Z3_model _model = 0;
Z3_literals _labels = 0;
Z3_lbool lb;
std::vector<Z3_ast> _assumptions(assumptions.size());
std::vector<Z3_ast> _interpolants(assumptions.size()-1);
for(unsigned i = 0; i < assumptions.size(); i++)
_assumptions[i] = assumptions[i];
std::vector<Z3_ast> _theory(theory.size());
for(unsigned i = 0; i < theory.size(); i++)
_theory[i] = theory[i];
lb = Z3_interpolate(
ctx(),
_assumptions.size(),
VEC2PTR(_assumptions),
0,
0,
VEC2PTR(_interpolants),
&_model,
&_labels,
incremental,
_theory.size(),
VEC2PTR(_theory));
if(lb == Z3_L_FALSE){
interpolants.resize(_interpolants.size());
for (unsigned i = 0; i < _interpolants.size(); ++i) {
interpolants[i] = expr(ctx(),_interpolants[i]);
}
}
if (_model) {
model = iz3wrapper::model(ctx(), _model);
}
if(_labels){
labels = _labels;
}
return lb;
}
#endif
static int linearize_assumptions(int num,
TermTree *assumptions,
std::vector<std::vector <expr> > &linear_assumptions,
std::vector<int> &parents){
for(unsigned i = 0; i < assumptions->getChildren().size(); i++)
num = linearize_assumptions(num, assumptions->getChildren()[i], linear_assumptions, parents);
// linear_assumptions[num].push_back(assumptions->getTerm());
for(unsigned i = 0; i < assumptions->getChildren().size(); i++)
parents[assumptions->getChildren()[i]->getNumber()] = num;
parents[num] = SHRT_MAX; // in case we have no parent
linear_assumptions[num].push_back(assumptions->getTerm());
std::vector<expr> &ts = assumptions->getTerms();
for(unsigned i = 0; i < ts.size(); i++)
linear_assumptions[num].push_back(ts[i]);
return num + 1;
}
static int unlinearize_interpolants(int num,
TermTree* assumptions,
const std::vector<expr> &interpolant,
TermTree * &tree_interpolant)
{
std::vector<TermTree *> chs(assumptions->getChildren().size());
for(unsigned i = 0; i < assumptions->getChildren().size(); i++)
num = unlinearize_interpolants(num, assumptions->getChildren()[i], interpolant,chs[i]);
expr f;
if(num < (int)interpolant.size()) // last interpolant is missing, presumed false
f = interpolant[num];
tree_interpolant = new TermTree(f,chs);
return num + 1;
}
lbool interpolating_solver::interpolate_tree(TermTree *assumptions,
TermTree *&interpolant,
model &model,
literals &labels,
bool incremental
)
{
int size = assumptions->number(0);
std::vector<std::vector<expr> > linear_assumptions(size);
std::vector<int> parents(size);
linearize_assumptions(0,assumptions,linear_assumptions,parents);
ptr_vector< ::ast> _interpolants(size-1);
vector<ptr_vector< ::ast> >_assumptions(size);
for(int i = 0; i < size; i++)
for(unsigned j = 0; j < linear_assumptions[i].size(); j++)
_assumptions[i].push_back(linear_assumptions[i][j]);
::vector<int> _parents; _parents.resize(parents.size());
for(unsigned i = 0; i < parents.size(); i++)
_parents[i] = parents[i];
ptr_vector< ::ast> _theory(theory.size());
for(unsigned i = 0; i < theory.size(); i++)
_theory[i] = theory[i];
if(!incremental){
push();
for(unsigned i = 0; i < linear_assumptions.size(); i++)
for(unsigned j = 0; j < linear_assumptions[i].size(); j++)
add(linear_assumptions[i][j]);
}
check_result res = unsat;
if(!m_solver->get_proof())
res = check();
if(res == unsat){
interpolation_options_struct opts;
if(weak_mode)
opts.set("weak","1");
::ast *proof = m_solver->get_proof();
try {
iz3interpolate(m(),proof,_assumptions,_parents,_interpolants,_theory,&opts);
}
// If there's an interpolation bug, throw a char *
// exception so duality can catch it and restart.
catch (const interpolation_failure &f) {
throw f.msg();
}
std::vector<expr> linearized_interpolants(_interpolants.size());
for(unsigned i = 0; i < _interpolants.size(); i++)
linearized_interpolants[i] = expr(ctx(),_interpolants[i]);
// since iz3interpolant returns interpolants with one ref count, we decrement here
for(unsigned i = 0; i < _interpolants.size(); i++)
m().dec_ref(_interpolants[i]);
unlinearize_interpolants(0,assumptions,linearized_interpolants,interpolant);
interpolant->setTerm(ctx().bool_val(false));
}
model_ref _m;
m_solver->get_model(_m);
model = Duality::model(ctx(),_m.get());
#if 0
if(_labels){
labels = _labels;
}
#endif
if(!incremental)
pop();
return (res == unsat) ? l_false : ((res == sat) ? l_true : l_undef);
}
void interpolating_solver::SetWeakInterpolants(bool weak){
weak_mode = weak;
}
void interpolating_solver::SetPrintToFile(const std::string &filename){
print_filename = filename;
}
void interpolating_solver::AssertInterpolationAxiom(const expr & t){
add(t);
theory.push_back(t);
}
void interpolating_solver::RemoveInterpolationAxiom(const expr & t){
// theory.remove(t);
}
const char *interpolating_solver::profile(){
// return Z3_interpolation_profile(ctx());
return "";
}
static void get_assumptions_rec(stl_ext::hash_set<ast> &memo, const proof &pf, std::vector<expr> &assumps){
if(memo.find(pf) != memo.end())return;
memo.insert(pf);
pfrule dk = pf.rule();
if(dk == PR_ASSERTED){
expr con = pf.conc();
assumps.push_back(con);
}
else {
unsigned nprems = pf.num_prems();
for(unsigned i = 0; i < nprems; i++){
proof arg = pf.prem(i);
get_assumptions_rec(memo,arg,assumps);
}
}
}
void proof::get_assumptions(std::vector<expr> &assumps){
stl_ext::hash_set<ast> memo;
get_assumptions_rec(memo,*this,assumps);
}
void ast::show() const{
std::cout << mk_pp(raw(), m()) << std::endl;
}
void model::show() const {
model_smt2_pp(std::cout, m(), *m_model, 0);
std::cout << std::endl;
}
void model::show_hash() const {
std::ostringstream ss;
model_smt2_pp(ss, m(), *m_model, 0);
hash_space::hash<std::string> hasher;
unsigned h = hasher(ss.str());
std::cout << "model hash: " << h << "\n";
}
void solver::show() {
unsigned n = m_solver->get_num_assertions();
if(!n)
return;
ast_smt_pp pp(m());
for (unsigned i = 0; i < n-1; ++i)
pp.add_assumption(m_solver->get_assertion(i));
pp.display_smt2(std::cout, m_solver->get_assertion(n-1));
}
void solver::print(const char *filename) {
std::ofstream f(filename);
unsigned n = m_solver->get_num_assertions();
if(!n)
return;
ast_smt_pp pp(m());
for (unsigned i = 0; i < n-1; ++i)
pp.add_assumption(m_solver->get_assertion(i));
pp.display_smt2(f, m_solver->get_assertion(n-1));
}
void solver::show_assertion_ids() {
#if 0
unsigned n = m_solver->get_num_assertions();
std::cerr << "assertion ids: ";
for (unsigned i = 0; i < n-1; ++i)
std::cerr << " " << m_solver->get_assertion(i)->get_id();
std::cerr << "\n";
#else
unsigned n = m_solver->get_num_assertions();
std::cerr << "assertion ids hash: ";
unsigned h = 0;
for (unsigned i = 0; i < n-1; ++i)
h += m_solver->get_assertion(i)->get_id();
std::cerr << h << "\n";
#endif
}
void include_ast_show(ast &a){
a.show();
}
void include_model_show(model &a){
a.show();
}
void show_ast(::ast *a, ast_manager &m) {
std::cout << mk_pp(a, m) << std::endl;
}
bool expr::is_label (bool &pos,std::vector<symbol> &names) const {
buffer< ::symbol> _names;
bool res = m().is_label(to_expr(raw()),pos,_names);
if(res)
for(unsigned i = 0; i < _names.size(); i++)
names.push_back(symbol(ctx(),_names[i]));
return res;
}
double current_time()
{
static stopwatch sw;
static bool started = false;
if(!started){
sw.start();
started = true;
}
return sw.get_current_seconds();
}
}

1489
src/duality/duality_wrapper.h
View file

File diff suppressed because it is too large Load diff

18
src/interp/CMakeLists.txt
View file

@ -1,18 +0,0 @@
z3_add_component(interp
SOURCES
iz3base.cpp
iz3checker.cpp
iz3interp.cpp
iz3mgr.cpp
iz3pp.cpp
iz3profiling.cpp
iz3proof.cpp
iz3proof_itp.cpp
iz3scopes.cpp
iz3translate.cpp
iz3translate_direct.cpp
COMPONENT_DEPENDENCIES
solver
PYG_FILES
interp_params.pyg
)

6
src/interp/interp_params.pyg
View file

@ -1,6 +0,0 @@
def_module_params('interp',
description='interpolation parameters',
export=True,
params=(('profile', BOOL, False, '(INTERP) profile interpolation'),
('check', BOOL, False, '(INTERP) check interpolants'),
))

372
src/interp/iz3base.cpp
View file

@ -1,372 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
iz3base.cpp
Abstract:
Base class for interpolators. Includes an AST manager and a scoping
object as bases.
Author:
Ken McMillan (kenmcmil)
Revision History:
--*/
#ifdef _WINDOWS
#pragma warning(disable:4996)
#pragma warning(disable:4800)
#pragma warning(disable:4267)
#pragma warning(disable:4101)
#endif
#include "interp/iz3base.h"
#include <stdio.h>
#include <fstream>
#include <iostream>
#include <ostream>
#include "solver/solver.h"
#include "../smt/smt_solver.h"
using namespace stl_ext;
iz3base::range &iz3base::ast_range(ast t){
return ast_ranges_hash[t].rng;
}
iz3base::range &iz3base::sym_range(symb d){
return sym_range_hash[d];
}
void iz3base::add_frame_range(int frame, ast t){
range &rng = ast_range(t);
if(!in_range(frame,rng)){
range_add(frame,rng);
for(int i = 0, n = num_args(t); i < n; ++i)
add_frame_range(frame,arg(t,i));
if(op(t) == Uninterpreted)
range_add(frame,sym_range(sym(t)));
}
}
#if 1
iz3base::range &iz3base::ast_scope(ast t){
ranges &rngs = ast_ranges_hash[t];
range &rng = rngs.scp;
if(!rngs.scope_computed){ // not computed yet
rng = range_full();
for(int i = 0, n = num_args(t); i < n; ++i)
rng = range_glb(rng,ast_scope(arg(t,i)));
if(op(t) == Uninterpreted)
if(parents.empty() || num_args(t) == 0) // in tree mode, all function syms are global
rng = range_glb(rng,sym_range(sym(t)));
rngs.scope_computed = true;
}
return rng;
}
#else
iz3base::range &iz3base::ast_scope(ast t){
ranges &rngs = ast_ranges_hash[t];
if(rngs.scope_computed) return rngs.scp;
range rng = range_full();
for(int i = 0, n = num_args(t); i < n; ++i)
rng = range_glb(rng,ast_scope(arg(t,i)));
if(op(t) == Uninterpreted)
if(parents.empty() || num_args(t) == 0) // in tree mode, all function syms are global
rng = range_glb(rng,sym_range(sym(t)));
rngs = ast_ranges_hash[t];
rngs.scope_computed = true;
rngs.scp = rng;
return rngs.scp;
}
#endif
void iz3base::print(const std::string &filename){
ast t = make(And,cnsts);
std::ofstream f(filename.c_str());
print_sat_problem(f,t);
f.close();
}
void iz3base::gather_conjuncts_rec(ast n, std::vector<ast> &conjuncts, stl_ext::hash_set<ast> &memo){
if(memo.find(n) == memo.end()){
memo.insert(n);
if(op(n) == And){
int nargs = num_args(n);
for(int i = 0; i < nargs; i++)
gather_conjuncts_rec(arg(n,i),conjuncts,memo);
}
else
conjuncts.push_back(n);
}
}
void iz3base::gather_conjuncts(ast n, std::vector<ast> &conjuncts){
hash_set<ast> memo;
gather_conjuncts_rec(n,conjuncts,memo);
}
bool iz3base::is_literal(ast n){
if(is_not(n))n = arg(n,0);
if(is_true(n) || is_false(n)) return false;
if(op(n) == And) return false;
return true;
}
iz3base::ast iz3base::simplify_and(std::vector<ast> &conjuncts){
hash_set<ast> memo;
for(unsigned i = 0; i < conjuncts.size(); i++){
if(is_false(conjuncts[i]))
return conjuncts[i];
if(is_true(conjuncts[i]) || memo.find(conjuncts[i]) != memo.end()){
std::swap(conjuncts[i],conjuncts.back());
conjuncts.pop_back();
}
else if(memo.find(mk_not(conjuncts[i])) != memo.end())
return mk_false(); // contradiction!
else
memo.insert(conjuncts[i]);
}
if(conjuncts.empty())return mk_true();
return make(And,conjuncts);
}
iz3base::ast iz3base::simplify_with_lit_rec(ast n, ast lit, stl_ext::hash_map<ast,ast> &memo, int depth){
if(is_not(n))return mk_not(simplify_with_lit_rec(mk_not(n),lit,memo,depth));
if(n == lit) return mk_true();
ast not_lit = mk_not(lit);
if(n == not_lit) return mk_false();
if(op(n) != And || depth <= 0) return n;
std::pair<ast,ast> foo(n,ast());
std::pair<hash_map<ast,ast>::iterator,bool> bar = memo.insert(foo);
ast &res = bar.first->second;
if(!bar.second) return res;
int nargs = num_args(n);
std::vector<ast> args(nargs);
for(int i = 0; i < nargs; i++)
args[i] = simplify_with_lit_rec(arg(n,i),lit,memo,depth-1);
res = simplify_and(args);
return res;
}
iz3base::ast iz3base::simplify_with_lit(ast n, ast lit){
hash_map<ast,ast> memo;
return simplify_with_lit_rec(n,lit,memo,1);
}
iz3base::ast iz3base::simplify(ast n){
if(is_not(n)) return mk_not(simplify(mk_not(n)));
std::pair<ast,ast> memo_obj(n,ast());
std::pair<hash_map<ast,ast>::iterator,bool> memo = simplify_memo.insert(memo_obj);
ast &res = memo.first->second;
if(!memo.second) return res;
switch(op(n)){
case And: {
std::vector<ast> conjuncts;
gather_conjuncts(n,conjuncts);
for(unsigned i = 0; i < conjuncts.size(); i++)
conjuncts[i] = simplify(conjuncts[i]);
#if 0
for(unsigned i = 0; i < conjuncts.size(); i++)
if(is_literal(conjuncts[i]))
for(unsigned j = 0; j < conjuncts.size(); j++)
if(j != i)
conjuncts[j] = simplify_with_lit(conjuncts[j],conjuncts[i]);
#endif
res = simplify_and(conjuncts);
}
break;
case Equal: {
ast x = arg(n,0);
ast y = arg(n,1);
if(ast_id(x) > ast_id(y))
std::swap(x,y);
res = make(Equal,x,y);
break;
}
default:
res = n;
}
return res;
}
void iz3base::initialize(const std::vector<ast> &_parts, const std::vector<int> &_parents, const std::vector<ast> &_theory){
cnsts = _parts;
theory = _theory;
for(unsigned i = 0; i < cnsts.size(); i++)
add_frame_range(i, cnsts[i]);
for(unsigned i = 0; i < _theory.size(); i++){
add_frame_range(SHRT_MIN, _theory[i]);
add_frame_range(SHRT_MAX, _theory[i]);
}
for(unsigned i = 0; i < cnsts.size(); i++)
frame_map[cnsts[i]] = i;
for(unsigned i = 0; i < theory.size(); i++)
frame_map[theory[i]] = INT_MAX;
}
void iz3base::initialize(const std::vector<std::vector<ast> > &_parts, const std::vector<int> &_parents, const std::vector<ast> &_theory){
cnsts.resize(_parts.size());
theory = _theory;
for(unsigned i = 0; i < _parts.size(); i++)
for(unsigned j = 0; j < _parts[i].size(); j++){
cnsts[i] = make(And,_parts[i]);
add_frame_range(i, _parts[i][j]);
frame_map[_parts[i][j]] = i;
}
for(unsigned i = 0; i < _theory.size(); i++){
add_frame_range(SHRT_MIN, _theory[i]);
add_frame_range(SHRT_MAX, _theory[i]);
frame_map[theory[i]] = INT_MAX;
}
}
void iz3base::check_interp(const std::vector<ast> &itps, std::vector<ast> &theory){
#if 0
Z3_config config = Z3_mk_config();
Z3_context vctx = Z3_mk_context(config);
int frames = cnsts.size();
std::vector<Z3_ast> foocnsts(cnsts);
for(unsigned i = 0; i < frames; i++)
foocnsts[i] = Z3_mk_implies(ctx,Z3_mk_true(ctx),cnsts[i]);
Z3_write_interpolation_problem(ctx,frames,&foocnsts[0],0, "temp_lemma.smt", theory.size(), &theory[0]);
int vframes,*vparents;
Z3_ast *vcnsts;
const char *verror;
bool ok = Z3_read_interpolation_problem(vctx,&vframes,&vcnsts,0,"temp_lemma.smt",&verror);
assert(ok);
std::vector<Z3_ast> vvcnsts(vframes);
std::copy(vcnsts,vcnsts+vframes,vvcnsts.begin());
std::vector<Z3_ast> vitps(itps.size());
for(unsigned i = 0; i < itps.size(); i++)
vitps[i] = Z3_mk_implies(ctx,Z3_mk_true(ctx),itps[i]);
Z3_write_interpolation_problem(ctx,itps.size(),&vitps[0],0,"temp_interp.smt");
int iframes,*iparents;
Z3_ast *icnsts;
const char *ierror;
ok = Z3_read_interpolation_problem(vctx,&iframes,&icnsts,0,"temp_interp.smt",&ierror);
assert(ok);
const char *error = 0;
bool iok = Z3_check_interpolant(vctx, frames, &vvcnsts[0], parents.size() ? &parents[0] : 0, icnsts, &error);
assert(iok);
#endif
}
bool iz3base::is_sat(const std::vector<ast> &q, ast &_proof, std::vector<ast> &vars){
params_ref p;
p.set_bool("proof", true); // this is currently useless
p.set_bool("model", true);
p.set_bool("unsat_core", true);
scoped_ptr<solver_factory> sf = mk_smt_solver_factory();
scoped_ptr< ::solver > solver = (*sf)(m(), p, true, true, true, ::symbol::null);
::solver &s = *solver.get();
for(unsigned i = 0; i < q.size(); i++)
s.assert_expr(to_expr(q[i].raw()));
lbool res = s.check_sat(0,nullptr);
if (m().canceled()) {
throw iz3_exception(Z3_CANCELED_MSG);
}
if(res == l_false){
::ast *proof = s.get_proof();
_proof = cook(proof);
}
else if(vars.size()) {
model_ref _m;
s.get_model(_m);
if (!_m.get()) {
SASSERT(l_undef == res);
throw iz3_exception("interpolation cannot proceed without a model");
}
for(unsigned i = 0; i < vars.size(); i++){
expr_ref r(m());
_m.get()->eval(to_expr(vars[i].raw()),r,true);
vars[i] = cook(r.get());
}
}
solver = nullptr;
return res != l_false;
}
void iz3base::find_children(const stl_ext::hash_set<ast> &cnsts_set,
const ast &tree,
std::vector<ast> &cnsts,
std::vector<int> &parents,
std::vector<ast> &conjuncts,
std::vector<int> &children,
std::vector<int> &pos_map,
bool merge
){
std::vector<int> my_children;
std::vector<ast> my_conjuncts;
if(op(tree) == Interp){ // if we've hit an interpolation position...
find_children(cnsts_set,arg(tree,0),cnsts,parents,my_conjuncts,my_children,pos_map,merge);
if(my_conjuncts.empty())
my_conjuncts.push_back(mk_true()); // need at least one conjunct
int root = cnsts.size() + my_conjuncts.size() - 1;
for(unsigned i = 0; i < my_conjuncts.size(); i++){
parents.push_back(root);
cnsts.push_back(my_conjuncts[i]);
}
for(unsigned i = 0; i < my_children.size(); i++)
parents[my_children[i]] = root;
children.push_back(root);
pos_map.push_back(root);
}
else {
if(op(tree) == And){
int nargs = num_args(tree);
for(int i = 0; i < nargs; i++)
find_children(cnsts_set,arg(tree,i),cnsts,parents,my_conjuncts,my_children,pos_map,merge);
}
if(cnsts_set.find(tree) != cnsts_set.end()){
if(merge && !my_conjuncts.empty())
my_conjuncts.back() = mk_and(my_conjuncts.back(),tree);
else
my_conjuncts.push_back(tree);
}
for(unsigned i = 0; i < my_children.size(); i++)
children.push_back(my_children[i]);
for(unsigned i = 0; i < my_conjuncts.size(); i++)
conjuncts.push_back(my_conjuncts[i]);
}
}
void iz3base::to_parents_vec_representation(const std::vector<ast> &_cnsts,
const ast &tree,
std::vector<ast> &cnsts,
std::vector<int> &parents,
std::vector<ast> &theory,
std::vector<int> &pos_map,
bool merge
){
std::vector<int> my_children;
std::vector<ast> my_conjuncts;
hash_set<ast> cnsts_set;
for(unsigned i = 0; i < _cnsts.size(); i++)
cnsts_set.insert(_cnsts[i]);
ast _tree = (op(tree) != Interp) ? make(Interp,tree) : tree;
find_children(cnsts_set,_tree,cnsts,parents,my_conjuncts,my_children,pos_map,merge);
if(op(tree) != Interp) pos_map.pop_back();
parents[parents.size()-1] = SHRT_MAX;
// rest of the constraints are the background theory
hash_set<ast> used_set;
for(unsigned i = 0; i < cnsts.size(); i++)
used_set.insert(cnsts[i]);
for(unsigned i = 0; i < _cnsts.size(); i++)
if(used_set.find(_cnsts[i]) == used_set.end())
theory.push_back(_cnsts[i]);
}

195
src/interp/iz3base.h
View file

@ -1,195 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
iz3base.h
Abstract:
Base class for interpolators. Includes an AST manager and a scoping
object as bases.
Author:
Ken McMillan (kenmcmil)
Revision History:
--*/
#ifndef IZ3BASE_H
#define IZ3BASE_H
#include "interp/iz3mgr.h"
#include "interp/iz3scopes.h"
namespace hash_space {
template <>
class hash<func_decl *> {
public:
size_t operator()(func_decl * const &s) const {
return (size_t) s;
}
};
}
/* Base class for interpolators. Includes an AST manager and a scoping
object as bases. */
class iz3base : public iz3mgr, public scopes {
public:
/** Get the range in which an expression occurs. This is the
smallest subtree containing all occurrences of the
expression. */
range &ast_range(ast);
/** Get the scope of an expression. This is the set of tree nodes in
which all of the expression's symbols are in scope. */
range &ast_scope(ast);
/** Get the range of a symbol. This is the smallest subtree containing
all occurrences of the symbol. */
range &sym_range(symb);
/** Is an expression local (in scope in some frame)? */
bool is_local(ast node){
return !range_is_empty(ast_scope(node));
}
/** Simplify an expression */
ast simplify(ast);
/** Constructor */
iz3base(ast_manager &_m_manager,
const std::vector<ast> &_cnsts,
const std::vector<int> &_parents,
const std::vector<ast> &_theory)
: iz3mgr(_m_manager), scopes(_parents) {
initialize(_cnsts,_parents,_theory);
weak = false;
}
iz3base(const iz3mgr& other,
const std::vector<ast> &_cnsts,
const std::vector<int> &_parents,
const std::vector<ast> &_theory)
: iz3mgr(other), scopes(_parents) {
initialize(_cnsts,_parents,_theory);
weak = false;
}
iz3base(const iz3mgr& other,
const std::vector<std::vector<ast> > &_cnsts,
const std::vector<int> &_parents,
const std::vector<ast> &_theory)
: iz3mgr(other), scopes(_parents) {
initialize(_cnsts,_parents,_theory);
weak = false;
}
iz3base(const iz3mgr& other)
: iz3mgr(other), scopes() {
weak = false;
}
/* Set our options */
void set_option(const std::string &name, const std::string &value){
if(name == "weak" && value == "1") weak = true;
}
/* Are we doing weak interpolants? */
bool weak_mode(){return weak;}
/** Print interpolation problem to an SMTLIB format file */
void print(const std::string &filename);
/** Check correctness of a solutino to this problem. */
void check_interp(const std::vector<ast> &itps, std::vector<ast> &theory);
/** For convenience -- is this formula SAT? */
bool is_sat(const std::vector<ast> &consts, ast &_proof, std::vector<ast> &vars);
/** Interpolator for clauses, to be implemented */
virtual void interpolate_clause(std::vector<ast> &lits, std::vector<ast> &itps){
throw iz3_exception("no interpolator");
}
ast get_proof_check_assump(range &rng){
std::vector<ast> cs(theory);
cs.push_back(cnsts[rng.hi]);
return make(And,cs);
}
int frame_of_assertion(const ast &ass){
stl_ext::hash_map<ast,int>::iterator it = frame_map.find(ass);
if(it == frame_map.end())
throw iz3_exception("unknown assertion");
return it->second;
}
void to_parents_vec_representation(const std::vector<ast> &_cnsts,
const ast &tree,
std::vector<ast> &cnsts,
std::vector<int> &parents,
std::vector<ast> &theory,
std::vector<int> &pos_map,
bool merge = false
);
protected:
std::vector<ast> cnsts;
std::vector<ast> theory;
private:
struct ranges {
range rng;
range scp;
bool scope_computed;
ranges(){scope_computed = false;}
};
stl_ext::hash_map<symb,range> sym_range_hash;
stl_ext::hash_map<ast,ranges> ast_ranges_hash;
stl_ext::hash_map<ast,ast> simplify_memo;
stl_ext::hash_map<ast,int> frame_map; // map assertions to frames
// int frames; // number of frames
protected:
void add_frame_range(int frame, ast t);
private:
void initialize(const std::vector<ast> &_parts, const std::vector<int> &_parents, const std::vector<ast> &_theory);
void initialize(const std::vector<std::vector<ast> > &_parts, const std::vector<int> &_parents, const std::vector<ast> &_theory);
bool is_literal(ast n);
void gather_conjuncts_rec(ast n, std::vector<ast> &conjuncts, stl_ext::hash_set<ast> &memo);
void gather_conjuncts(ast n, std::vector<ast> &conjuncts);
ast simplify_and(std::vector<ast> &conjuncts);
ast simplify_with_lit_rec(ast n, ast lit, stl_ext::hash_map<ast,ast> &memo, int depth);
ast simplify_with_lit(ast n, ast lit);
void find_children(const stl_ext::hash_set<ast> &cnsts_set,
const ast &tree,
std::vector<ast> &cnsts,
std::vector<int> &parents,
std::vector<ast> &conjuncts,
std::vector<int> &children,
std::vector<int> &pos_map,
bool merge
);
bool weak;
};
#endif

227
src/interp/iz3checker.cpp
View file

@ -1,227 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
iz3checker.cpp
Abstract:
check correctness of interpolant
Author:
Ken McMillan (kenmcmil)
Revision History:
--*/
#ifdef _WINDOWS
#pragma warning(disable:4996)
#pragma warning(disable:4800)
#pragma warning(disable:4267)
#pragma warning(disable:4101)
#endif
#include "interp/iz3base.h"
#include "interp/iz3checker.h"
#include <algorithm>
#include <stdio.h>
#include <fstream>
#include <sstream>
#include <iostream>
#include <set>
#include <iterator>
using namespace stl_ext;
struct iz3checker : iz3base {
/* HACK: for tree interpolants, we assume that uninterpreted functions
are global. This is because in the current state of the tree interpolation
code, symbols that appear in sibling sub-trees have to be global, and
we have no way to eliminate such function symbols. When tree interpolation is
fixed, we can tree function symbols the same as constant symbols. */
bool is_tree;
void support(const ast &t, std::set<std::string> &res, hash_set<ast> &memo){
if(memo.find(t) != memo.end()) return;
memo.insert(t);
int nargs = num_args(t);
for(int i = 0; i < nargs; i++)
support(arg(t,i),res,memo);
switch(op(t)){
case Uninterpreted:
if(nargs == 0 || !is_tree) {
std::string name = string_of_symbol(sym(t));
res.insert(name);
}
break;
case Forall:
case Exists:
support(get_quantifier_body(t),res,memo);
break;
default:;
}
}
bool check(solver *s, std::ostream &err,
const std::vector<ast> &cnsts,
const std::vector<int> &parents,
const std::vector<ast> &itp,
const std::vector<ast> &theory){
is_tree = !parents.empty();
int num = cnsts.size();
std::vector<std::vector<int> > children(num);
for(int i = 0; i < num-1; i++){
if(parents.size())
children[parents[i]].push_back(i);
else
children[i+1].push_back(i);
}
for(int i = 0; i < num; i++){
s->push();
for(unsigned j = 0; j < theory.size(); j++)
s->assert_expr(to_expr(theory[j].raw()));
s->assert_expr(to_expr(cnsts[i].raw()));
std::vector<int> &cs = children[i];
for(unsigned j = 0; j < cs.size(); j++)
s->assert_expr(to_expr(itp[cs[j]].raw()));
if(i != num-1)
s->assert_expr(to_expr(mk_not(itp[i]).raw()));
lbool result = s->check_sat(0,nullptr);
if(result != l_false){
err << "interpolant " << i << " is incorrect";
s->pop(1);
for(unsigned j = 0; j < theory.size(); j++)
s->assert_expr(to_expr(theory[j].raw()));
for(unsigned j = 0; j < cnsts.size(); j++)
if(in_range(j,range_downward(i)))
s->assert_expr(to_expr(cnsts[j].raw()));
if(i != num-1)
s->assert_expr(to_expr(mk_not(itp[i]).raw()));
lbool result = s->check_sat(0,nullptr);
if(result != l_false)
err << "interpolant " << i << " is not implied by its downeard closurn";
return false;
}
s->pop(1);
}
std::vector<std::set<std::string> > supports(num);
for(int i = 0; i < num; i++){
hash_set<ast> memo;
support(cnsts[i],supports[i],memo);
}
for(int i = 0; i < num-1; i++){
std::vector<bool> Bside(num);
for(int j = num-1; j >= 0; j--)
Bside[j] = j != i;
for(int j = num-1; j >= 0; j--)
if(!Bside[j]){
std::vector<int> &cs = children[i];
for(unsigned k = 0; k < cs.size(); k++)
Bside[cs[k]] = false;
}
std::set<std::string> Asup, Bsup,common,Isup,bad;
for(int j = num-1; j >= 0; j--){
std::set<std::string> &side = Bside[j] ? Bsup : Asup;
side.insert(supports[j].begin(),supports[j].end());
}
std::set_intersection(Asup.begin(),Asup.end(),Bsup.begin(),Bsup.end(),std::inserter(common,common.begin()));
{
hash_set<ast> tmemo;
for(unsigned j = 0; j < theory.size(); j++)
support(theory[j],common,tmemo); // all theory symbols allowed in interps
}
hash_set<ast> memo;
support(itp[i],Isup,memo);
std::set_difference(Isup.begin(),Isup.end(),common.begin(),common.end(),std::inserter(bad,bad.begin()));
if(!bad.empty()){
err << "bad symbols in interpolant " << i << ":";
std::copy(bad.begin(),bad.end(),std::ostream_iterator<std::string>(err,","));
return false;
}
}
return true;
}
bool check(solver *s, std::ostream &err,
const std::vector<ast> &_cnsts,
const ast &tree,
const std::vector<ast> &itp){
std::vector<int> pos_map;
// convert to the parents vector representation
to_parents_vec_representation(_cnsts, tree, cnsts, parents, theory, pos_map);
//use the parents vector representation to compute interpolant
return check(s,err,cnsts,parents,itp,theory);
}
iz3checker(ast_manager &_m)
: iz3base(_m) {
}
iz3checker(iz3mgr &_m)
: iz3base(_m) {
}
};
template <class T>
std::vector<T> to_std_vector(const ::vector<T> &v){
std::vector<T> _v(v.size());
for(unsigned i = 0; i < v.size(); i++)
_v[i] = v[i];
return _v;
}
bool iz3check(ast_manager &_m_manager,
solver *s,
std::ostream &err,
const ptr_vector<ast> &cnsts,
const ::vector<int> &parents,
const ptr_vector<ast> &interps,
const ptr_vector<ast> &theory)
{
iz3checker chk(_m_manager);
return chk.check(s,err,chk.cook(cnsts),to_std_vector(parents),chk.cook(interps),chk.cook(theory));
}
bool iz3check(iz3mgr &mgr,
solver *s,
std::ostream &err,
const std::vector<iz3mgr::ast> &cnsts,
const std::vector<int> &parents,
const std::vector<iz3mgr::ast> &interps,
const std::vector<iz3mgr::ast> &theory)
{
iz3checker chk(mgr);
return chk.check(s,err,cnsts,parents,interps,theory);
}
bool iz3check(ast_manager &_m_manager,
solver *s,
std::ostream &err,
const ptr_vector<ast> &_cnsts,
ast *tree,
const ptr_vector<ast> &interps)
{
iz3checker chk(_m_manager);
return chk.check(s,err,chk.cook(_cnsts),chk.cook(tree),chk.cook(interps));
}

49
src/interp/iz3checker.h
View file

@ -1,49 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
iz3checker.h
Abstract:
check correctness of an interpolant
Author:
Ken McMillan (kenmcmil)
Revision History:
--*/
#ifndef IZ3_CHECKER_H
#define IZ3_CHECKER_H
#include "interp/iz3mgr.h"
#include "solver/solver.h"
bool iz3check(ast_manager &_m_manager,
solver *s,
std::ostream &err,
const ptr_vector<ast> &cnsts,
const ::vector<int> &parents,
const ptr_vector<ast> &interps,
const ptr_vector<ast> &theory);
bool iz3check(ast_manager &_m_manager,
solver *s,
std::ostream &err,
const ptr_vector<ast> &cnsts,
ast *tree,
const ptr_vector<ast> &interps);
bool iz3check(iz3mgr &mgr,
solver *s,
std::ostream &err,
const std::vector<iz3mgr::ast> &cnsts,
const std::vector<int> &parents,
const std::vector<iz3mgr::ast> &interps,
const ptr_vector<iz3mgr::ast> &theory);
#endif

28
src/interp/iz3exception.h
View file

@ -1,28 +0,0 @@
/*++
Copyright (c) 2015 Microsoft Corporation
Module Name:
iz3exception.h
Abstract:
Base class for exceptions raised by interpolation routines
Author:
Notes:
--*/
#ifndef _IZ3EXCEPTION_H_
#define _IZ3EXCEPTION_H_
#include "util/z3_exception.h"
#include "util/error_codes.h"
class iz3_exception: public default_exception {
public:
iz3_exception(const std::string &msg): default_exception(msg) {}
};
#endif

479
src/interp/iz3hash.h
View file

@ -1,479 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
iz3hash.h
Abstract:
Simple implementation of bucket-list hash tables conforming to SGI
hash_map and hash_set interfaces. Just enough members are
implemented to support iz3 and duality.
iz3 and duality need this package because they assume that insert
preserves iterators and references to elements, which is not true
of the hashtable packages in util.
This package lives in namespace hash_space. Specializations of
class "hash" should be made in this namespace.
Author:
Ken McMillan (kenmcmil)
Revision History:
--*/
#ifndef IZ3_HASH_H
#define IZ3_HASH_H
#ifdef _WINDOWS
#pragma warning(disable:4267)
#endif
#include <string>
#include <vector>
#include <iterator>
#include "util/hash.h"
#define stl_ext hash_space
namespace hash_space {
template <typename T> class hash {};
template <>
class hash<int> {
public:
size_t operator()(const int &s) const {
return s;
}
};
template <>
class hash<std::string> {
public:
size_t operator()(const std::string &s) const {
return string_hash(s.c_str(), s.size(), 0);
}
};
template <>
class hash<std::pair<int,int> > {
public:
size_t operator()(const std::pair<int,int> &p) const {
return p.first + p.second;
}
};
template <class T>
class hash<std::pair<T *, T *> > {
public:
size_t operator()(const std::pair<T *,T *> &p) const {
return (size_t)p.first + (size_t)p.second;
}
};
enum { num_primes = 29 };
static const unsigned long primes[num_primes] =
{
7ul,
53ul,
97ul,
193ul,
389ul,
769ul,
1543ul,
3079ul,
6151ul,
12289ul,
24593ul,
49157ul,
98317ul,
196613ul,
393241ul,
786433ul,
1572869ul,
3145739ul,
6291469ul,
12582917ul,
25165843ul,
50331653ul,
100663319ul,
201326611ul,
402653189ul,
805306457ul,
1610612741ul,
3221225473ul,
4294967291ul
};
inline unsigned long next_prime(unsigned long n) {
const unsigned long* to = primes + (int)num_primes;
for(const unsigned long* p = primes; p < to; p++)
if(*p >= n) return *p;
return primes[num_primes-1];
}
template<class Value, class Key, class HashFun, class GetKey, class KeyEqFun>
class hashtable
{
public:
typedef Value &reference;
typedef const Value &const_reference;
struct Entry
{
Entry* next;
Value val;
Entry(const Value &_val) : val(_val) {next = nullptr;}
};
struct iterator
{
Entry* ent;
hashtable* tab;
typedef std::forward_iterator_tag iterator_category;
typedef Value value_type;
typedef std::ptrdiff_t difference_type;
typedef size_t size_type;
typedef Value& reference;
typedef Value* pointer;
iterator(Entry* _ent, hashtable* _tab) : ent(_ent), tab(_tab) { }
iterator() { }
Value &operator*() const { return ent->val; }
Value *operator->() const { return &(operator*()); }
iterator &operator++() {
Entry *old = ent;
ent = ent->next;
if (!ent) {
size_t bucket = tab->get_bucket(old->val);
while (!ent && ++bucket < tab->buckets.size())
ent = tab->buckets[bucket];
}
return *this;
}
iterator operator++(int) {
iterator tmp = *this;
operator++();
return tmp;
}
bool operator==(const iterator& it) const {
return ent == it.ent;
}
bool operator!=(const iterator& it) const {
return ent != it.ent;
}
};
struct const_iterator
{
const Entry* ent;
const hashtable* tab;
typedef std::forward_iterator_tag iterator_category;
typedef Value value_type;
typedef std::ptrdiff_t difference_type;
typedef size_t size_type;
typedef const Value& reference;
typedef const Value* pointer;
const_iterator(const Entry* _ent, const hashtable* _tab) : ent(_ent), tab(_tab) { }
const_iterator() { }
const Value &operator*() const { return ent->val; }
const Value *operator->() const { return &(operator*()); }
const_iterator &operator++() {
Entry *old = ent;
ent = ent->next;
if (!ent) {
size_t bucket = tab->get_bucket(old->val);
while (!ent && ++bucket < tab->buckets.size())
ent = tab->buckets[bucket];
}
return *this;
}
const_iterator operator++(int) {
const_iterator tmp = *this;
operator++();
return tmp;
}
bool operator==(const const_iterator& it) const {
return ent == it.ent;
}
bool operator!=(const const_iterator& it) const {
return ent != it.ent;
}
};
private:
typedef std::vector<Entry*> Table;
Table buckets;
size_t entries;
HashFun hash_fun ;
GetKey get_key;
KeyEqFun key_eq_fun;
public:
hashtable(size_t init_size) : buckets(init_size,(Entry *)nullptr) {
entries = 0;
}
hashtable(const hashtable& other) {
dup(other);
}
hashtable& operator= (const hashtable& other) {
if (&other != this)
dup(other);
return *this;
}
~hashtable() {
clear();
}
size_t size() const {
return entries;
}
bool empty() const {
return size() == 0;
}
void swap(hashtable& other) {
buckets.swap(other.buckets);
std::swap(entries, other.entries);
}
iterator begin() {
for (size_t i = 0; i < buckets.size(); ++i)
if (buckets[i])
return iterator(buckets[i], this);
return end();
}
iterator end() {
return iterator(nullptr, this);
}
const_iterator begin() const {
for (size_t i = 0; i < buckets.size(); ++i)
if (buckets[i])
return const_iterator(buckets[i], this);
return end();
}
const_iterator end() const {
return const_iterator(nullptr, this);
}
size_t get_bucket(const Value& val, size_t n) const {
return hash_fun(get_key(val)) % n;
}
size_t get_key_bucket(const Key& key) const {
return hash_fun(key) % buckets.size();
}
size_t get_bucket(const Value& val) const {
return get_bucket(val,buckets.size());
}
Entry *lookup(const Value& val, bool ins = false)
{
resize(entries + 1);
size_t n = get_bucket(val);
Entry* from = buckets[n];
for (Entry* ent = from; ent; ent = ent->next)
if (key_eq_fun(get_key(ent->val), get_key(val)))
return ent;
if(!ins) return nullptr;
Entry* tmp = new Entry(val);
tmp->next = from;
buckets[n] = tmp;
++entries;
return tmp;
}
Entry *lookup_key(const Key& key) const
{
size_t n = get_key_bucket(key);
Entry* from = buckets[n];
for (Entry* ent = from; ent; ent = ent->next)
if (key_eq_fun(get_key(ent->val), key))
return ent;
return nullptr;
}
const_iterator find(const Key& key) const {
return const_iterator(lookup_key(key),this);
}
iterator find(const Key& key) {
return iterator(lookup_key(key),this);
}
std::pair<iterator,bool> insert(const Value& val){
size_t old_entries = entries;
Entry *ent = lookup(val,true);
return std::pair<iterator,bool>(iterator(ent,this),entries > old_entries);
}
iterator insert(const iterator &it, const Value& val){
Entry *ent = lookup(val,true);
return iterator(ent,this);
}
size_t erase(const Key& key)
{
Entry** p = &(buckets[get_key_bucket(key)]);
size_t count = 0;
while(*p){
Entry *q = *p;
if (key_eq_fun(get_key(q->val), key)) {
++count;
*p = q->next;
delete q;
}
else
p = &(q->next);
}
entries -= count;
return count;
}
void resize(size_t new_size) {
const size_t old_n = buckets.size();
if (new_size <= old_n) return;
const size_t n = next_prime(new_size);
if (n <= old_n) return;
Table tmp(n, (Entry*)nullptr);
for (size_t i = 0; i < old_n; ++i) {
Entry* ent = buckets[i];
while (ent) {
size_t new_bucket = get_bucket(ent->val, n);
buckets[i] = ent->next;
ent->next = tmp[new_bucket];
tmp[new_bucket] = ent;
ent = buckets[i];
}
}
buckets.swap(tmp);
}
void clear()
{
for (size_t i = 0; i < buckets.size(); ++i) {
for (Entry* ent = buckets[i]; ent != nullptr;) {
Entry* next = ent->next;
delete ent;
ent = next;
}
buckets[i] = nullptr;
}
entries = 0;
}
void dup(const hashtable& other)
{
buckets.resize(other.buckets.size());
for (size_t i = 0; i < other.buckets.size(); ++i) {
Entry** to = &buckets[i];
for (Entry* from = other.buckets[i]; from; from = from->next)
to = &((*to = new Entry(from->val))->next);
}
entries = other.entries;
}
};
template <typename T>
class equal {
public:
bool operator()(const T& x, const T &y) const {
return x == y;
}
};
template <typename T>
class identity {
public:
const T &operator()(const T &x) const {
return x;
}
};
template <typename T, typename U>
class proj1 {
public:
const T &operator()(const std::pair<T,U> &x) const {
return x.first;
}
};
template <typename Element, class HashFun = hash<Element>,
class EqFun = equal<Element> >
class hash_set
: public hashtable<Element,Element,HashFun,identity<Element>,EqFun> {
public:
typedef Element value_type;
hash_set()
: hashtable<Element,Element,HashFun,identity<Element>,EqFun>(7) {}
};
template <typename Key, typename Value, class HashFun = hash<Key>,
class EqFun = equal<Key> >
class hash_map
: public hashtable<std::pair<Key,Value>,Key,HashFun,proj1<Key,Value>,EqFun> {
public:
hash_map()
: hashtable<std::pair<Key,Value>,Key,HashFun,proj1<Key,Value>,EqFun>(7) {}
Value &operator[](const Key& key) {
std::pair<Key,Value> kvp(key,Value());
return
hashtable<std::pair<Key,Value>,Key,HashFun,proj1<Key,Value>,EqFun>::
lookup(kvp,true)->val.second;
}
};
}
#endif

578
src/interp/iz3interp.cpp
View file

@ -1,578 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
iz3interp.cpp
Abstract:
Interpolation based on proof translation.
Author:
Ken McMillan (kenmcmil)
Revision History:
--*/
/* Copyright 2011 Microsoft Research. */
#ifdef _WINDOWS
#pragma warning(disable:4996)
#pragma warning(disable:4800)
#pragma warning(disable:4267)
#pragma warning(disable:4101)
#endif
#include <algorithm>
#include <stdio.h>
#include <fstream>
#include <sstream>
#include <set>
#include <iostream>
#include "interp/iz3profiling.h"
#include "interp/iz3translate.h"
#include "interp/iz3proof.h"
#include "interp/iz3hash.h"
#include "interp/iz3interp.h"
#include "ast/scoped_proof.h"
using namespace stl_ext;
#if 1
struct frame_reducer : public iz3mgr {
int frames;
hash_map<ast,int> frame_map;
std::vector<int> assertions_map;
std::vector<int> orig_parents_copy;
std::vector<bool> used_frames;
frame_reducer(const iz3mgr &other)
: iz3mgr(other) {}
void get_proof_assumptions_rec(z3pf proof, hash_set<ast> &memo, std::vector<bool> &used_frames){
if(memo.find(proof) != memo.end())return;
memo.insert(proof);
pfrule dk = pr(proof);
if(dk == PR_ASSERTED){
ast con = conc(proof);
if(frame_map.find(con) != frame_map.end()){ // false for theory facts
int frame = frame_map[con];
used_frames[frame] = true;
}
}
else {
unsigned nprems = num_prems(proof);
for(unsigned i = 0; i < nprems; i++){
z3pf arg = prem(proof,i);
get_proof_assumptions_rec(arg,memo,used_frames);
}
}
}
void get_frames(const std::vector<std::vector<ast> >&z3_preds,
const std::vector<int> &orig_parents,
std::vector<std::vector<ast> >&assertions,
std::vector<int> &parents,
z3pf proof){
frames = z3_preds.size();
orig_parents_copy = orig_parents;
for(unsigned i = 0; i < z3_preds.size(); i++)
for(unsigned j = 0; j < z3_preds[i].size(); j++)
frame_map[z3_preds[i][j]] = i;
used_frames.resize(frames);
hash_set<ast> memo;
get_proof_assumptions_rec(proof,memo,used_frames);
std::vector<int> assertions_back_map(frames);
// if multiple children of a tree node are used, we can't delete it
std::vector<int> used_children;
used_children.reserve(frames);
for(int i = 0; i < frames; i++)
used_children.push_back(0);
for(int i = 0; i < frames; i++)
if(orig_parents[i] != SHRT_MAX)
if(used_frames[i] || used_children[i]){
if(used_children[i] > 1)
used_frames[i] = true;
used_children[orig_parents[i]]++;
}
for(unsigned i = 0; i < z3_preds.size(); i++)
if(used_frames[i] || i == z3_preds.size() - 1){
assertions.push_back(z3_preds[i]);
assertions_map.push_back(i);
assertions_back_map[i] = assertions.size() - 1;
}
if(orig_parents.size()){
parents.resize(assertions.size());
for(unsigned i = 0; i < assertions.size(); i++){
int p = orig_parents[assertions_map[i]];
while(p != SHRT_MAX && !used_frames[p])
p = orig_parents[p];
parents[i] = p == SHRT_MAX ? p : assertions_back_map[p];
}
}
// std::cout << "used frames = " << frames << "\n";
}
void fix_interpolants(std::vector<ast> &interpolants){
std::vector<ast> unfixed = interpolants;
interpolants.resize(frames - 1);
for(int i = 0; i < frames - 1; i++)
interpolants[i] = mk_true();
for(unsigned i = 0; i < unfixed.size(); i++)
interpolants[assertions_map[i]] = unfixed[i];
for(int i = 0; i < frames-2; i++){
int p = orig_parents_copy.size() == 0 ? i+1 : orig_parents_copy[i];
if(p < frames - 1 && !used_frames[p])
interpolants[p] = mk_and(interpolants[i],interpolants[p]);
}
}
};
#else
struct frame_reducer {
frame_reducer(context _ctx){
}
void get_frames(const std::vector<ast> &z3_preds,
const std::vector<int> &orig_parents,
std::vector<ast> &assertions,
std::vector<int> &parents,
ast proof){
assertions = z3_preds;
parents = orig_parents;
}
void fix_interpolants(std::vector<ast> &interpolants){
}
};
#endif
template<class T>
struct killme {
T *p;
killme(){p = nullptr;}
void set(T *_p) {p = _p;}
~killme(){
if(p)
delete p;
}
};
class iz3interp : public iz3base {
public:
killme<iz3secondary> sp_killer;
killme<iz3translation> tr_killer;
bool is_linear(std::vector<int> &parents){
for(int i = 0; i < ((int)parents.size())-1; i++)
if(parents[i] != i+1)
return false;
return true;
}
void test_secondary(const std::vector<ast> &cnsts,
const std::vector<int> &parents,
std::vector<ast> &interps
){
throw iz3_exception("secondary interpolating prover not supported");
}
void proof_to_interpolant(z3pf proof,
const std::vector<std::vector<ast> > &cnsts,
const std::vector<int> &parents,
std::vector<ast> &interps,
const std::vector<ast> &theory,
interpolation_options_struct *options = nullptr
){
#if 0
test_secondary(cnsts,parents,interps);
return;
#endif
profiling::timer_start("Interpolation prep");
// get rid of frames not used in proof
std::vector<std::vector<ast> > cnsts_vec;
std::vector<int> parents_vec;
frame_reducer fr(*this);
fr.get_frames(cnsts,parents,cnsts_vec,parents_vec,proof);
int num = cnsts_vec.size();
std::vector<ast> interps_vec(num-1);
// if this is really a sequence problem, we can make it easier
if(is_linear(parents_vec))
parents_vec.clear();
// secondary prover no longer supported
iz3secondary *sp = nullptr;
#define BINARY_INTERPOLATION
#ifndef BINARY_INTERPOLATION
// create a translator
iz3translation *tr = iz3translation::create(*this,sp,cnsts_vec,parents_vec,theory);
tr_killer.set(tr);
// set the translation options, if needed
if(options)
for(hash_map<std::string,std::string>::iterator it = options->map.begin(), en = options->map.end(); it != en; ++it)
tr->set_option(it->first, it->second);
// create a proof object to hold the translation
iz3proof pf(tr);
profiling::timer_stop("Interpolation prep");
// translate into an interpolatable proof
profiling::timer_start("Proof translation");
try {
tr->translate(proof,pf);
}
catch (const char *msg) {
throw interpolation_failure(msg);
}
catch (const iz3translation::unsupported & ex) {
TRACE("iz3", tout << "unsupported " << "\n";);
throw interpolation_error();
}
catch (const iz3proof::proof_error & ex) {
TRACE("iz3", tout << "proof error " << "\n";);
throw interpolation_error();
}
profiling::timer_stop("Proof translation");
// translate the proof into interpolants
profiling::timer_start("Proof interpolation");
for(int i = 0; i < num-1; i++){
interps_vec[i] = pf.interpolate(tr->range_downward(i),tr->weak_mode());
interps_vec[i] = tr->quantify(interps_vec[i],tr->range_downward(i));
}
profiling::timer_stop("Proof interpolation");
#else
iz3base the_base(*this,cnsts_vec,parents_vec,theory);
profiling::timer_stop("Interpolation prep");
for(int i = 0; i < num-1; i++){
range rng = the_base.range_downward(i);
std::vector<std::vector<ast> > cnsts_vec_vec(2);
for(unsigned j = 0; j < cnsts_vec.size(); j++){
bool is_A = the_base.in_range(j,rng);
for(unsigned k = 0; k < cnsts_vec[j].size(); k++)
cnsts_vec_vec[is_A ? 0 : 1].push_back(cnsts_vec[j][k]);
}
killme<iz3translation> tr_killer_i;
iz3translation *tr = iz3translation::create(*this,sp,cnsts_vec_vec,std::vector<int>(),theory);
tr_killer_i.set(tr);
// set the translation options, if needed
if(options)
for(hash_map<std::string,std::string>::iterator it = options->map.begin(), en = options->map.end(); it != en; ++it)
tr->set_option(it->first, it->second);
// create a proof object to hold the translation
iz3proof pf(tr);
// translate into an interpolatable proof
profiling::timer_start("Proof translation");
try {
tr->translate(proof,pf);
}
catch (const char *msg) {
throw interpolation_failure(msg);
}
catch (const iz3translation::unsupported & ex) {
TRACE("iz3", tout << "unsupported " << "\n";);
throw interpolation_error();
}
catch (const iz3proof::proof_error &) {
TRACE("iz3", tout << "proof error\n";);
throw interpolation_error();
}
profiling::timer_stop("Proof translation");
// translate the proof into interpolants
profiling::timer_start("Proof interpolation");
interps_vec[i] = pf.interpolate(tr->range_downward(0),tr->weak_mode());
interps_vec[i] = tr->quantify(interps_vec[i],tr->range_downward(0));
profiling::timer_stop("Proof interpolation");
}
#endif
// put back in the removed frames
fr.fix_interpolants(interps_vec);
interps = interps_vec;
}
void proof_to_interpolant(z3pf proof,
std::vector<ast> &cnsts,
const std::vector<int> &parents,
std::vector<ast> &interps,
const std::vector<ast> &theory,
interpolation_options_struct *options = nullptr
){
std::vector<std::vector<ast> > cnsts_vec(cnsts.size());
for(unsigned i = 0; i < cnsts.size(); i++)
cnsts_vec[i].push_back(cnsts[i]);
proof_to_interpolant(proof,cnsts_vec,parents,interps,theory,options);
}
// same as above, but represents the tree using an ast
void proof_to_interpolant(const z3pf &proof,
const std::vector<ast> &_cnsts,
const ast &tree,
std::vector<ast> &interps,
interpolation_options_struct *options = nullptr
){
std::vector<int> pos_map;
// convert to the parents vector representation
to_parents_vec_representation(_cnsts, tree, cnsts, parents, theory, pos_map);
//use the parents vector representation to compute interpolant
proof_to_interpolant(proof,cnsts,parents,interps,theory,options);
// get the interps for the tree positions
std::vector<ast> _interps = interps;
interps.resize(pos_map.size());
for(unsigned i = 0; i < pos_map.size(); i++){
unsigned j = pos_map[i];
interps[i] = j < _interps.size() ? _interps[j] : mk_false();
}
}
bool has_interp(hash_map<ast,bool> &memo, const ast &t){
if(memo.find(t) != memo.end())
return memo[t];
bool res = false;
if(op(t) == Interp)
res = true;
else if(op(t) == And){
int nargs = num_args(t);
for(int i = 0; i < nargs; i++)
res |= has_interp(memo, arg(t,i));
}
memo[t] = res;
return res;
}
void collect_conjuncts(std::vector<ast> &cnsts, hash_map<ast,bool> &memo, const ast &t){
if(!has_interp(memo,t))
cnsts.push_back(t);
else {
int nargs = num_args(t);
for(int i = 0; i < nargs; i++)
collect_conjuncts(cnsts, memo, arg(t,i));
}
}
void assert_conjuncts(solver &s, std::vector<ast> &cnsts, const ast &t){
hash_map<ast,bool> memo;
collect_conjuncts(cnsts,memo,t);
for(unsigned i = 0; i < cnsts.size(); i++)
s.assert_expr(to_expr(cnsts[i].raw()));
}
void get_proof_assumptions(z3pf proof, std::vector<ast> &cnsts, hash_set<ast> &memo){
if(memo.find(proof) != memo.end())return;
memo.insert(proof);
pfrule dk = pr(proof);
if(dk == PR_ASSERTED)
cnsts.push_back(conc(proof));
else {
unsigned nprems = num_prems(proof);
for(unsigned i = 0; i < nprems; i++){
z3pf arg = prem(proof,i);
get_proof_assumptions(arg,cnsts,memo);
}
}
}
iz3interp(ast_manager &_m_manager)
: iz3base(_m_manager) {}
};
void iz3interpolate(ast_manager &_m_manager,
ast *proof,
const ptr_vector<ast> &cnsts,
const ::vector<int> &parents,
ptr_vector<ast> &interps,
const ptr_vector<ast> &theory,
interpolation_options_struct * options)
{
iz3interp itp(_m_manager);
if(options)
options->apply(itp);
std::vector<iz3mgr::ast> _cnsts(cnsts.size());
std::vector<int> _parents(parents.size());
std::vector<iz3mgr::ast> _interps;
std::vector<iz3mgr::ast> _theory(theory.size());
for(unsigned i = 0; i < cnsts.size(); i++)
_cnsts[i] = itp.cook(cnsts[i]);
for(unsigned i = 0; i < parents.size(); i++)
_parents[i] = parents[i];
for(unsigned i = 0; i < theory.size(); i++)
_theory[i] = itp.cook(theory[i]);
iz3mgr::ast _proof = itp.cook(proof);
itp.proof_to_interpolant(_proof,_cnsts,_parents,_interps,_theory,options);
interps.resize(_interps.size());
for(unsigned i = 0; i < interps.size(); i++)
interps[i] = itp.uncook(_interps[i]);
}
void iz3interpolate(ast_manager &_m_manager,
ast *proof,
const ::vector<ptr_vector<ast> > &cnsts,
const ::vector<int> &parents,
ptr_vector<ast> &interps,
const ptr_vector<ast> &theory,
interpolation_options_struct * options)
{
iz3interp itp(_m_manager);
if(options)
options->apply(itp);
std::vector<std::vector<iz3mgr::ast> > _cnsts(cnsts.size());
std::vector<int> _parents(parents.size());
std::vector<iz3mgr::ast> _interps;
std::vector<iz3mgr::ast> _theory(theory.size());
for(unsigned i = 0; i < cnsts.size(); i++)
for(unsigned j = 0; j < cnsts[i].size(); j++)
_cnsts[i].push_back(itp.cook(cnsts[i][j]));
for(unsigned i = 0; i < parents.size(); i++)
_parents[i] = parents[i];
for(unsigned i = 0; i < theory.size(); i++)
_theory[i] = itp.cook(theory[i]);
iz3mgr::ast _proof = itp.cook(proof);
itp.proof_to_interpolant(_proof,_cnsts,_parents,_interps,_theory,options);
interps.resize(_interps.size());
for(unsigned i = 0; i < interps.size(); i++)
interps[i] = itp.uncook(_interps[i]);
}
void iz3interpolate(ast_manager &_m_manager,
ast *proof,
const ptr_vector<ast> &cnsts,
ast *tree,
ptr_vector<ast> &interps,
interpolation_options_struct * options)
{
iz3interp itp(_m_manager);
if(options)
options->apply(itp);
std::vector<iz3mgr::ast> _cnsts(cnsts.size());
std::vector<iz3mgr::ast> _interps;
for(unsigned i = 0; i < cnsts.size(); i++)
_cnsts[i] = itp.cook(cnsts[i]);
iz3mgr::ast _proof = itp.cook(proof);
iz3mgr::ast _tree = itp.cook(tree);
// if consts isn't provided, we can reconstruct it
if(_cnsts.empty()){
hash_set<iz3mgr::ast> memo;
itp.get_proof_assumptions(_proof,_cnsts,memo);
}
itp.proof_to_interpolant(_proof,_cnsts,_tree,_interps,options);
interps.resize(_interps.size());
for(unsigned i = 0; i < interps.size(); i++)
interps[i] = itp.uncook(_interps[i]);
}
lbool iz3interpolate(ast_manager &_m_manager,
solver &s,
ast *tree,
ptr_vector<ast> &cnsts,
ptr_vector<ast> &interps,
model_ref &m,
interpolation_options_struct * options)
{
iz3interp itp(_m_manager);
if(options)
options->apply(itp);
iz3mgr::ast _tree = itp.cook(tree);
std::vector<iz3mgr::ast> _cnsts;
itp.assert_conjuncts(s,_cnsts,_tree);
profiling::timer_start("solving");
lbool res = s.check_sat(0,nullptr);
profiling::timer_stop("solving");
if(res == l_false){
ast *proof = s.get_proof();
iz3mgr::ast _proof = itp.cook(proof);
std::vector<iz3mgr::ast> _interps;
itp.proof_to_interpolant(_proof,_cnsts,_tree,_interps,options);
interps.resize(_interps.size());
for(unsigned i = 0; i < interps.size(); i++)
interps[i] = itp.uncook(_interps[i]);
}
else if(m){
s.get_model(m);
}
cnsts.resize(_cnsts.size());
for(unsigned i = 0; i < cnsts.size(); i++)
cnsts[i] = itp.uncook(_cnsts[i]);
return res;
}
void interpolation_options_struct::apply(iz3base &b){
for(stl_ext::hash_map<std::string,std::string>::iterator it = map.begin(), en = map.end();
it != en;
++it)
b.set_option((*it).first,(*it).second);
}
// On linux and mac, unlimit stack space so we get recursion
#if defined(_WINDOWS) || defined(_CYGWIN) || defined(_MINGW)
#else
#include <sys/time.h>
#include <sys/resource.h>
class iz3stack_unlimiter {
public:
iz3stack_unlimiter() {
struct rlimit rl = {RLIM_INFINITY, RLIM_INFINITY};
setrlimit(RLIMIT_STACK, &rl);
// nothing to be done if above fails
}
};
// initializing this will unlimit stack
iz3stack_unlimiter the_iz3stack_unlimiter;
#endif

123
src/interp/iz3interp.h
View file

@ -1,123 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
iz3interp.h
Abstract:
Interpolation based on proof translation.
Author:
Ken McMillan (kenmcmil)
Revision History:
--*/
#ifndef IZ3_INTERP_H
#define IZ3_INTERP_H
#include "interp/iz3hash.h"
#include "interp/iz3exception.h"
#include "solver/solver.h"
class iz3base;
struct interpolation_options_struct {
stl_ext::hash_map<std::string,std::string> map;
public:
void set(const std::string &name, const std::string &value){
map[name] = value;
}
void apply(iz3base &b);
};
/** This object is thrown if a tree interpolation problem is mal-formed */
struct iz3_bad_tree: public iz3_exception {
iz3_bad_tree(): iz3_exception("iz3_bad_tree") {}
};
/** This object is thrown when iz3 fails due to an incompleteness in
the secondary solver. */
struct iz3_incompleteness: public iz3_exception {
iz3_incompleteness(): iz3_exception("iz3_incompleteness") {}
};
// This is thrown if there is some bug in the
// interpolation procedure
class interpolation_failure : public default_exception {
public:
interpolation_failure(const char *msg)
: default_exception(msg)
{
}
};
// This is thrown if we cannot derive an interpolant from a proof
// because it contains unsupported theories or if the proof contains
// errors
class interpolation_error : public default_exception {
public:
interpolation_error()
: default_exception("theory not supported by interpolation or bad proof" )
{
}
};
typedef interpolation_options_struct *interpolation_options;
/* Compute an interpolant from a proof. This version uses the parents vector
representation, for compatibility with the old API. */
void iz3interpolate(ast_manager &_m_manager,
ast *proof,
const ptr_vector<ast> &cnsts,
const ::vector<int> &parents,
ptr_vector<ast> &interps,
const ptr_vector<ast> &theory,
interpolation_options_struct * options = nullptr);
/* Same as above, but each constraint is a vector of formulas. */
void iz3interpolate(ast_manager &_m_manager,
ast *proof,
const vector<ptr_vector<ast> > &cnsts,
const ::vector<int> &parents,
ptr_vector<ast> &interps,
const ptr_vector<ast> &theory,
interpolation_options_struct * options = nullptr);
/* Compute an interpolant from a proof. This version uses the ast
representation, for compatibility with the new API. Here, cnsts is
a vector of all the assertions in the proof. This can be
over-approximated by the set of all assertions in the
solver. However, if it is empty it will be reconstructed from the
proof, so it can be considered a hint. */
void iz3interpolate(ast_manager &_m_manager,
ast *proof,
const ptr_vector<ast> &cnsts,
ast *tree,
ptr_vector<ast> &interps,
interpolation_options_struct * options);
/* Compute an interpolant from an ast representing an interpolation
problem, if unsat, else return a model (if enabled). Uses the
given solver to produce the proof/model. Also returns a vector
of the constraints in the problem, helpful for checking correctness.
*/
lbool iz3interpolate(ast_manager &_m_manager,
solver &s,
ast *tree,
ptr_vector<ast> &cnsts,
ptr_vector<ast> &interps,
model_ref &m,
interpolation_options_struct * options);
#endif

969
src/interp/iz3mgr.cpp
View file

@ -1,969 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
iz3mgr.cpp
Abstract:
A wrapper around an ast manager, providing convenience methods.
Author:
Ken McMillan (kenmcmil)
Revision History:
--*/
#ifdef _WINDOWS
#pragma warning(disable:4996)
#pragma warning(disable:4800)
#pragma warning(disable:4267)
#pragma warning(disable:4101)
#pragma warning(disable:4805)
#pragma warning(disable:4800)
#endif
#include "interp/iz3mgr.h"
#include <stdio.h>
#include <fstream>
#include <iostream>
#include <ostream>
#include <sstream>
#include "ast/expr_abstract.h"
#include "util/params.h"
#include "ast/used_vars.h"
using namespace stl_ext;
std::ostream &operator <<(std::ostream &s, const iz3mgr::ast &a){
return s;
}
iz3mgr::ast iz3mgr::make_var(const std::string &name, type ty){
symbol s = symbol(name.c_str());
return cook(m().mk_const(m().mk_const_decl(s, ty)));
}
iz3mgr::ast iz3mgr::make(opr op, int n, raw_ast **args){
switch(op) {
case True: return mki(m_basic_fid,OP_TRUE,n,args);
case False: return mki(m_basic_fid,OP_FALSE,n,args);
case Equal: return mki(m_basic_fid,OP_EQ,n,args);
case Distinct: return mki(m_basic_fid,OP_DISTINCT,n,args);
case Ite: return mki(m_basic_fid,OP_ITE,n,args);
case And: return mki(m_basic_fid,OP_AND,n,args);
case Or: return mki(m_basic_fid,OP_OR,n,args);
case Iff: return mki(m_basic_fid,OP_IFF,n,args);
case Xor: return mki(m_basic_fid,OP_XOR,n,args);
case Not: return mki(m_basic_fid,OP_NOT,n,args);
case Implies: return mki(m_basic_fid,OP_IMPLIES,n,args);
case Oeq: return mki(m_basic_fid,OP_OEQ,n,args);
case Interp: return mki(m_basic_fid,OP_INTERP,n,args);
case Leq: return mki(m_arith_fid,OP_LE,n,args);
case Geq: return mki(m_arith_fid,OP_GE,n,args);
case Lt: return mki(m_arith_fid,OP_LT,n,args);
case Gt: return mki(m_arith_fid,OP_GT,n,args);
case Plus: return mki(m_arith_fid,OP_ADD,n,args);
case Sub: return mki(m_arith_fid,OP_SUB,n,args);
case Uminus: return mki(m_arith_fid,OP_UMINUS,n,args);
case Times: return mki(m_arith_fid,OP_MUL,n,args);
case Div: return mki(m_arith_fid,OP_DIV,n,args);
case Idiv: return mki(m_arith_fid,OP_IDIV,n,args);
case Rem: return mki(m_arith_fid,OP_REM,n,args);
case Mod: return mki(m_arith_fid,OP_MOD,n,args);
case Power: return mki(m_arith_fid,OP_POWER,n,args);
case ToReal: return mki(m_arith_fid,OP_TO_REAL,n,args);
case ToInt: return mki(m_arith_fid,OP_TO_INT,n,args);
case IsInt: return mki(m_arith_fid,OP_IS_INT,n,args);
case Store: return mki(m_array_fid,OP_STORE,n,args);
case Select: return mki(m_array_fid,OP_SELECT,n,args);
case ConstArray: return mki(m_array_fid,OP_CONST_ARRAY,n,args);
case ArrayDefault: return mki(m_array_fid,OP_ARRAY_DEFAULT,n,args);
case ArrayMap: return mki(m_array_fid,OP_ARRAY_MAP,n,args);
case SetUnion: return mki(m_array_fid,OP_SET_UNION,n,args);
case SetIntersect: return mki(m_array_fid,OP_SET_INTERSECT,n,args);
case SetDifference: return mki(m_array_fid,OP_SET_DIFFERENCE,n,args);
case SetComplement: return mki(m_array_fid,OP_SET_COMPLEMENT,n,args);
case SetSubSet: return mki(m_array_fid,OP_SET_SUBSET,n,args);
case AsArray: return mki(m_array_fid,OP_AS_ARRAY,n,args);
default:
assert(0);
return ast();
}
}
iz3mgr::ast iz3mgr::mki(family_id fid, decl_kind dk, int n, raw_ast **args){
return cook(m().mk_app(fid, dk, 0, nullptr, n, (expr **)args));
}
iz3mgr::ast iz3mgr::make(opr op, const std::vector<ast> &args){
static std::vector<raw_ast*> a(10);
if(a.size() < args.size())
a.resize(args.size());
for(unsigned i = 0; i < args.size(); i++)
a[i] = args[i].raw();
return make(op,args.size(), args.size() ? &a[0] : nullptr);
}
iz3mgr::ast iz3mgr::make(opr op){
return make(op,0,nullptr);
}
iz3mgr::ast iz3mgr::make(opr op, const ast &arg0){
raw_ast *a = arg0.raw();
return make(op,1,&a);
}
iz3mgr::ast iz3mgr::make(opr op, const ast &arg0, const ast &arg1){
raw_ast *args[2];
args[0] = arg0.raw();
args[1] = arg1.raw();
return make(op,2,args);
}
iz3mgr::ast iz3mgr::make(opr op, const ast &arg0, const ast &arg1, const ast &arg2){
raw_ast *args[3];
args[0] = arg0.raw();
args[1] = arg1.raw();
args[2] = arg2.raw();
return make(op,3,args);
}
iz3mgr::ast iz3mgr::make(symb sym, int n, raw_ast **args){
return cook(m().mk_app(sym, n, (expr **) args));
}
iz3mgr::ast iz3mgr::make(symb sym, const std::vector<ast> &args){
static std::vector<raw_ast*> a(10);
if(a.size() < args.size())
a.resize(args.size());
for(unsigned i = 0; i < args.size(); i++)
a[i] = args[i].raw();
return make(sym,args.size(), args.size() ? &a[0] : nullptr);
}
iz3mgr::ast iz3mgr::make(symb sym){
return make(sym,0,nullptr);
}
iz3mgr::ast iz3mgr::make(symb sym, const ast &arg0){
raw_ast *a = arg0.raw();
return make(sym,1,&a);
}
iz3mgr::ast iz3mgr::make(symb sym, const ast &arg0, const ast &arg1){
raw_ast *args[2];
args[0] = arg0.raw();
args[1] = arg1.raw();
return make(sym,2,args);
}
iz3mgr::ast iz3mgr::make(symb sym, const ast &arg0, const ast &arg1, const ast &arg2){
raw_ast *args[3];
args[0] = arg0.raw();
args[1] = arg1.raw();
args[2] = arg2.raw();
return make(sym,3,args);
}
iz3mgr::ast iz3mgr::make_quant(opr op, const std::vector<ast> &bvs, ast &body){
if(bvs.size() == 0) return body;
std::vector<raw_ast *> foo(bvs.size());
std::vector<symbol> names;
std::vector<class sort *> types;
std::vector<expr *> bound_asts;
unsigned num_bound = bvs.size();
for (unsigned i = 0; i < num_bound; ++i) {
app* a = to_app(bvs[i].raw());
symbol s(to_app(a)->get_decl()->get_name());
names.push_back(s);
types.push_back(m().get_sort(a));
bound_asts.push_back(a);
}
expr_ref abs_body(m());
expr_abstract(m(), 0, num_bound, &bound_asts[0], to_expr(body.raw()), abs_body);
expr_ref result(m());
result = m().mk_quantifier(
op == Forall,
names.size(), &types[0], &names[0], abs_body.get(),
0,
symbol("itp"),
symbol(),
0, nullptr,
0, nullptr
);
return cook(result.get());
}
// FIXME replace this with existing Z3 functionality
iz3mgr::ast iz3mgr::clone(const ast &t, const std::vector<ast> &_args){
if(_args.size() == 0)
return t;
ast_manager& m = m_manager;
expr* a = to_expr(t.raw());
static std::vector<raw_ast*> rargs(10);
if(rargs.size() < _args.size())
rargs.resize(_args.size());
for(unsigned i = 0; i < _args.size(); i++)
rargs[i] = _args[i].raw();
expr* const* args = (expr **)&rargs[0];
switch(a->get_kind()) {
case AST_APP: {
app* e = to_app(a);
if (e->get_num_args() != _args.size()) {
assert(0);
}
else {
a = m.mk_app(e->get_decl(), _args.size(), args);
}
break;
}
case AST_QUANTIFIER: {
if (_args.size() != 1) {
assert(0);
}
else {
a = m.update_quantifier(to_quantifier(a), args[0]);
}
break;
}
default:
break;
}
return cook(a);
}
void iz3mgr::show(ast t){
if(t.null()){
std::cout << "(null)" << std::endl;
}
params_ref p;
p.set_bool("flat_assoc",false);
std::cout << mk_pp(t.raw(), m(), p) << std::endl;
}
void iz3mgr::show_symb(symb s){
std::cout << mk_pp(s, m()) << std::endl;
}
void iz3mgr::print_expr(std::ostream &s, const ast &e){
params_ref p;
p.set_bool("flat_assoc",false);
s << mk_pp(e.raw(), m(), p);
}
void iz3mgr::print_clause(std::ostream &s, std::vector<ast> &cls){
s << "(";
for(unsigned i = 0; i < cls.size(); i++){
if(i > 0) s << ",";
print_expr(s,cls[i]);
}
s << ")";
}
void iz3mgr::show_clause(std::vector<ast> &cls){
print_clause(std::cout,cls);
std::cout << std::endl;
}
void iz3mgr::print_lit(ast lit){
ast abslit = is_not(lit) ? arg(lit,0) : lit;
int f = op(abslit);
if(f == And || f == Or || f == Iff){
if(is_not(lit)) std::cout << "~";
std::cout << "[" << abslit << "]";
}
else
std::cout << lit;
}
static int pretty_cols = 79;
static int pretty_indent_chars = 2;
static int pretty_find_delim(const std::string &s, int pos){
int level = 0;
int end = s.size();
for(; pos < end; pos++){
int ch = s[pos];
if(ch == '(')level++;
if(ch == ')')level--;
if(level < 0 || (level == 0 && ch == ','))break;
}
return pos;
}
static void pretty_newline(std::ostream &f, int indent){
f << std::endl;
for(int i = 0; i < indent; i++)
f << " ";
}
void iz3mgr::pretty_print(std::ostream &f, const std::string &s){
int cur_indent = 0;
int indent = 0;
int col = 0;
int pos = 0;
while(pos < (int)s.size()){
int delim = pretty_find_delim(s,pos);
if(s[pos] != ')' && s[pos] != ',' && cur_indent > indent){
pretty_newline(f,indent);
cur_indent = indent;
col = indent;
continue;
}
if (col + delim - pos > pretty_cols) {
if (col > indent) {
pretty_newline(f,indent);
cur_indent = indent;
col = indent;
continue;
}
int paren = s.find('(',pos);
if(paren != (int)std::string::npos){
int chars = paren - pos + 1;
f << s.substr(pos,chars);
indent += pretty_indent_chars;
if(col) pretty_newline(f,indent);
cur_indent = indent;
pos += chars;
col = indent;
continue;
}
}
int chars = delim - pos + 1;
f << s.substr(pos,chars);
pos += chars;
col += chars;
if(s[delim] == ')')
indent -= pretty_indent_chars;
}
}
iz3mgr::opr iz3mgr::op(const ast &t){
ast_kind dk = t.raw()->get_kind();
switch(dk){
case AST_APP: {
expr * e = to_expr(t.raw());
func_decl *d = to_app(t.raw())->get_decl();
if (null_family_id == d->get_family_id())
return Uninterpreted;
// return (opr)d->get_decl_kind();
if (m_basic_fid == d->get_family_id()) {
switch(d->get_decl_kind()) {
case OP_TRUE: return True;
case OP_FALSE: return False;
case OP_EQ: return Equal;
case OP_DISTINCT: return Distinct;
case OP_ITE: return Ite;
case OP_AND: return And;
case OP_OR: return Or;
case OP_IFF: return Iff;
case OP_XOR: return Xor;
case OP_NOT: return Not;
case OP_IMPLIES: return Implies;
case OP_OEQ: return Oeq;
case OP_INTERP: return Interp;
default:
return Other;
}
}
if (m_arith_fid == d->get_family_id()) {
switch(d->get_decl_kind()) {
case OP_LE: return Leq;
case OP_GE: return Geq;
case OP_LT: return Lt;
case OP_GT: return Gt;
case OP_ADD: return Plus;
case OP_SUB: return Sub;
case OP_UMINUS: return Uminus;
case OP_MUL: return Times;
case OP_DIV: return Div;
case OP_IDIV: return Idiv;
case OP_REM: return Rem;
case OP_MOD: return Mod;
case OP_POWER: return Power;
case OP_TO_REAL: return ToReal;
case OP_TO_INT: return ToInt;
case OP_IS_INT: return IsInt;
default:
if (m().is_unique_value(e))
return Numeral;
return Other;
}
}
if (m_array_fid == d->get_family_id()) {
switch(d->get_decl_kind()) {
case OP_STORE: return Store;
case OP_SELECT: return Select;
case OP_CONST_ARRAY: return ConstArray;
case OP_ARRAY_DEFAULT: return ArrayDefault;
case OP_ARRAY_MAP: return ArrayMap;
case OP_SET_UNION: return SetUnion;
case OP_SET_INTERSECT: return SetIntersect;
case OP_SET_DIFFERENCE: return SetDifference;
case OP_SET_COMPLEMENT: return SetComplement;
case OP_SET_SUBSET: return SetSubSet;
case OP_AS_ARRAY: return AsArray;
default:
return Other;
}
}
return Other;
}
case AST_QUANTIFIER:
return to_quantifier(t.raw())->is_forall() ? Forall : Exists;
case AST_VAR:
return Variable;
default:;
}
return Other;
}
iz3mgr::pfrule iz3mgr::pr(const ast &t){
func_decl *d = to_app(t.raw())->get_decl();
assert(m_basic_fid == d->get_family_id());
return d->get_decl_kind();
}
void iz3mgr::print_sat_problem(std::ostream &out, const ast &t){
ast_smt_pp pp(m());
pp.set_simplify_implies(false);
pp.display_smt2(out, to_expr(t.raw()));
}
iz3mgr::ast iz3mgr::z3_simplify(const ast &e){
::expr * a = to_expr(e.raw());
params_ref p;
th_rewriter m_rw(m(), p);
expr_ref result(m());
m_rw(a, result);
return cook(result);
}
iz3mgr::ast iz3mgr::z3_really_simplify(const ast &e){
::expr * a = to_expr(e.raw());
params_ref simp_params;
simp_params.set_bool(":som",true);
simp_params.set_bool(":sort-sums",true);
th_rewriter m_rw(m(), simp_params);
expr_ref result(m());
m_rw(a, result);
return cook(result);
}
#if 0
static rational lcm(const rational &x, const rational &y){
int a = x.numerator();
int b = y.numerator();
return rational(a * b / gcd(a, b));
}
#endif
static rational extract_lcd(std::vector<rational> &res){
if(res.size() == 0) return rational(1); // shouldn't happen
rational lcd = denominator(res[0]);
for(unsigned i = 1; i < res.size(); i++)
lcd = lcm(lcd,denominator(res[i]));
for(unsigned i = 0; i < res.size(); i++)
res[i] *= lcd;
return lcd;
}
void iz3mgr::get_farkas_coeffs(const ast &proof, std::vector<ast>& coeffs){
std::vector<rational> rats;
get_farkas_coeffs(proof,rats);
coeffs.resize(rats.size());
for(unsigned i = 0; i < rats.size(); i++){
class sort *is = m().mk_sort(m_arith_fid, INT_SORT);
ast coeff = cook(m_arith_util.mk_numeral(rats[i],is));
coeffs[i] = coeff;
}
}
static void abs_rat(std::vector<rational> &rats){
// check that they are all non-neg -- if neg, take abs val and warn!
for(unsigned i = 0; i < rats.size(); i++)
if(rats[i].is_neg()){
// std::cout << "negative Farkas coeff!\n";
rats[i] = -rats[i];
}
}
bool iz3mgr::is_farkas_coefficient_negative(const ast &proof, int n){
rational r;
symb s = sym(proof);
bool ok = s->get_parameter(n+2).is_rational(r);
if(!ok)
throw iz3_exception("Bad Farkas coefficient");
return r.is_neg();
}
void iz3mgr::get_farkas_coeffs(const ast &proof, std::vector<rational>& rats){
symb s = sym(proof);
int numps = s->get_num_parameters();
rats.resize(numps-2);
#if 0
if(num_prems(proof) < numps-2){
std::cout << "bad farkas rule: " << num_prems(proof) << " premises should be " << numps-2 << "\n";
}
#endif
for(int i = 2; i < numps; i++){
rational r;
bool ok = s->get_parameter(i).is_rational(r);
if(!ok)
throw iz3_exception("Bad Farkas coefficient");
#if 0
{
ast con = conc(prem(proof,i-2));
ast temp = make_real(r); // for debugging
opr o = is_not(con) ? op(arg(con,0)) : op(con);
if(is_not(con) ? (o == Leq || o == Lt) : (o == Geq || o == Gt))
r = -r;
}
#endif
rats[i-2] = r;
}
#if 0
if(rats.size() != 0 && rats[0].is_neg()){
for(unsigned i = 0; i < rats.size(); i++){
assert(rats[i].is_neg());
rats[i] = -rats[i];
}
}
#endif
abs_rat(rats);
extract_lcd(rats);
}
void iz3mgr::get_broken_gcd_test_coeffs(const ast &proof, std::vector<rational>& rats){
symb s = sym(proof);
int numps = s->get_num_parameters();
rats.resize(numps-2);
for(int i = 2; i < numps; i++){
rational r;
bool ok = s->get_parameter(i).is_rational(r);
if(!ok)
throw "Bad Farkas coefficient";
rats[i-2] = r;
}
extract_lcd(rats);
}
void iz3mgr::get_assign_bounds_coeffs(const ast &proof, std::vector<ast>& coeffs){
std::vector<rational> rats;
get_assign_bounds_coeffs(proof,rats);
coeffs.resize(rats.size());
for(unsigned i = 0; i < rats.size(); i++){
coeffs[i] = make_int(rats[i]);
}
}
void iz3mgr::get_assign_bounds_coeffs(const ast &proof, std::vector<rational>& rats){
symb s = sym(proof);
int numps = s->get_num_parameters();
rats.resize(numps-1);
rats[0] = rational(1);
ast conseq = arg(conc(proof),0);
opr conseq_o = is_not(conseq) ? op(arg(conseq,0)) : op(conseq);
bool conseq_neg = is_not(conseq) ? (conseq_o == Leq || conseq_o == Lt) : (conseq_o == Geq || conseq_o == Gt);
for(int i = 2; i < numps; i++){
rational r;
bool ok = s->get_parameter(i).is_rational(r);
if(!ok)
throw iz3_exception("Bad Farkas coefficient");
{
ast con = arg(conc(proof),i-1);
ast temp = make_real(r); // for debugging
opr o = is_not(con) ? op(arg(con,0)) : op(con);
if(is_not(con) ? (o == Leq || o == Lt) : (o == Geq || o == Gt))
r = -r;
if(conseq_neg)
r = -r;
}
rats[i-1] = r;
}
#if 0
if(rats[1].is_neg()){ // work around bug -- if all coeffs negative, negate them
for(unsigned i = 1; i < rats.size(); i++){
if(!rats[i].is_neg())
throw iz3_exception("Bad Farkas coefficients");
rats[i] = -rats[i];
}
}
#endif
abs_rat(rats);
extract_lcd(rats);
}
void iz3mgr::get_gomory_cut_coeffs(const ast &proof, std::vector<ast>& coeffs){
std::vector<rational> rats;
get_gomory_cut_coeffs(proof,rats);
coeffs.resize(rats.size());
for(unsigned i = 0; i < rats.size(); i++){
coeffs[i] = make_int(rats[i]);
}
}
void iz3mgr::get_gomory_cut_coeffs(const ast &proof, std::vector<rational>& rats){
symb s = sym(proof);
int numps = s->get_num_parameters();
rats.resize(numps-2);
for(int i = 2; i < numps; i++){
rational r;
bool ok = s->get_parameter(i).is_rational(r);
if(!ok)
throw "Bad Farkas coefficient";
rats[i-2] = r;
}
abs_rat(rats);
extract_lcd(rats);
}
void iz3mgr::get_assign_bounds_rule_coeffs(const ast &proof, std::vector<ast>& coeffs){
std::vector<rational> rats;
get_assign_bounds_rule_coeffs(proof,rats);
coeffs.resize(rats.size());
for(unsigned i = 0; i < rats.size(); i++){
coeffs[i] = make_int(rats[i]);
}
}
void iz3mgr::get_assign_bounds_rule_coeffs(const ast &proof, std::vector<rational>& rats){
symb s = sym(proof);
int numps = s->get_num_parameters();
rats.resize(numps-1);
rats[0] = rational(1);
ast conseq = arg(conc(proof),0);
opr conseq_o = is_not(conseq) ? op(arg(conseq,0)) : op(conseq);
bool conseq_neg = is_not(conseq) ? (conseq_o == Leq || conseq_o == Lt) : (conseq_o == Geq || conseq_o == Gt);
for(int i = 2; i < numps; i++){
rational r;
bool ok = s->get_parameter(i).is_rational(r);
if(!ok)
throw iz3_exception("Bad Farkas coefficient");
{
ast con = conc(prem(proof,i-2));
ast temp = make_real(r); // for debugging
opr o = is_not(con) ? op(arg(con,0)) : op(con);
if(is_not(con) ? (o == Leq || o == Lt) : (o == Geq || o == Gt))
r = -r;
if(conseq_neg)
r = -r;
}
rats[i-1] = r;
}
#if 0
if(rats[1].is_neg()){ // work around bug -- if all coeffs negative, negate them
for(unsigned i = 1; i < rats.size(); i++){
if(!rats[i].is_neg())
throw iz3_exception("Bad Farkas coefficients");
rats[i] = -rats[i];
}
}
#endif
abs_rat(rats);
extract_lcd(rats);
}
/** Set P to P + cQ, where P and Q are linear inequalities. Assumes P is 0 <= y or 0 < y. */
void iz3mgr::linear_comb(ast &P, const ast &c, const ast &Q, bool round_off){
ast Qrhs;
bool qstrict = false;
if(is_not(Q)){
ast nQ = arg(Q,0);
switch(op(nQ)){
case Gt:
Qrhs = make(Sub,arg(nQ,1),arg(nQ,0));
break;
case Lt:
Qrhs = make(Sub,arg(nQ,0),arg(nQ,1));
break;
case Geq:
Qrhs = make(Sub,arg(nQ,1),arg(nQ,0));
qstrict = true;
break;
case Leq:
Qrhs = make(Sub,arg(nQ,0),arg(nQ,1));
qstrict = true;
break;
default:
throw iz3_exception("not an inequality");
}
}
else {
switch(op(Q)){
case Leq:
Qrhs = make(Sub,arg(Q,1),arg(Q,0));
break;
case Geq:
Qrhs = make(Sub,arg(Q,0),arg(Q,1));
break;
case Lt:
Qrhs = make(Sub,arg(Q,1),arg(Q,0));
qstrict = true;
break;
case Gt:
Qrhs = make(Sub,arg(Q,0),arg(Q,1));
qstrict = true;
break;
default:
throw iz3_exception("not an inequality");
}
}
bool pstrict = op(P) == Lt;
if (round_off && get_type(Qrhs) != int_type())
round_off = false;
if(qstrict && round_off && (pstrict || !(c == make_int(rational(1))))){
Qrhs = make(Sub,Qrhs,make_int(rational(1)));
qstrict = false;
}
Qrhs = make(Times,c,Qrhs);
bool strict = pstrict || qstrict;
if(strict)
P = make(Lt,arg(P,0),make(Plus,arg(P,1),Qrhs));
else
P = make(Leq,arg(P,0),make(Plus,arg(P,1),Qrhs));
}
iz3mgr::ast iz3mgr::sum_inequalities(const std::vector<ast> &coeffs, const std::vector<ast> &ineqs, bool round_off){
ast zero = make_int("0");
ast thing = make(Leq,zero,zero);
for(unsigned i = 0; i < ineqs.size(); i++){
linear_comb(thing,coeffs[i],ineqs[i], round_off);
}
thing = simplify_ineq(thing);
return thing;
}
void iz3mgr::mk_idiv(const ast& t, const rational &d, ast &whole, ast &frac){
opr o = op(t);
if(o == Plus){
int nargs = num_args(t);
for(int i = 0; i < nargs; i++)
mk_idiv(arg(t,i),d,whole,frac);
return;
}
else if(o == Times){
rational coeff;
if(is_numeral(arg(t,0),coeff)){
if(gcd(coeff,d) == d){
whole = make(Plus,whole,make(Times,make_int(coeff/d),arg(t,1)));
return;
}
}
}
frac = make(Plus,frac,t);
}
iz3mgr::ast iz3mgr::mk_idiv(const ast& q, const rational &d){
ast t = z3_simplify(q);
if(d == rational(1))
return t;
else {
ast whole = make_int("0");
ast frac = whole;
mk_idiv(t,d,whole,frac);
return z3_simplify(make(Plus,whole,make(Idiv,z3_simplify(frac),make_int(d))));
}
}
iz3mgr::ast iz3mgr::mk_idiv(const ast& t, const ast &d){
rational r;
if(is_numeral(d,r))
return mk_idiv(t,r);
return make(Idiv,t,d);
}
// does variable occur in expression?
int iz3mgr::occurs_in1(stl_ext::hash_map<ast,bool> &occurs_in_memo,ast var, ast e){
std::pair<ast,bool> foo(e,false);
std::pair<hash_map<ast,bool>::iterator,bool> bar = occurs_in_memo.insert(foo);
bool &res = bar.first->second;
if(bar.second){
if(e == var) res = true;
int nargs = num_args(e);
for(int i = 0; i < nargs; i++)
res |= occurs_in1(occurs_in_memo,var,arg(e,i));
}
return res;
}
int iz3mgr::occurs_in(ast var, ast e){
hash_map<ast,bool> memo;
return occurs_in1(memo,var,e);
}
bool iz3mgr::solve_arith(const ast &v, const ast &x, const ast &y, ast &res){
if(occurs_in(v,y))
return false;
if(op(x) == Plus){
int n = num_args(x);
for(int i = 0; i < n; i++){
if(arg(x,i) == v){
res = z3_simplify(make(Sub, y, make(Sub, x, v)));
return true;
}
}
}
return false;
}
// find a controlling equality for a given variable v in a term
// a controlling equality is of the form v = t, which, being
// false would force the formula to have the specifid truth value
// returns t, or null if no such
iz3mgr::ast iz3mgr::cont_eq(stl_ext::hash_set<ast> &cont_eq_memo, bool truth, ast v, ast e){
if(is_not(e)) return cont_eq(cont_eq_memo, !truth,v,arg(e,0));
if(cont_eq_memo.find(e) != cont_eq_memo.end())
return ast();
cont_eq_memo.insert(e);
if(!truth && op(e) == Equal){
if(arg(e,0) == v && !occurs_in(v,arg(e,1))) return(arg(e,1));
if(arg(e,1) == v && !occurs_in(v,arg(e,0))) return(arg(e,0));
ast res;
if(solve_arith(v,arg(e,0),arg(e,1),res)) return res;
if(solve_arith(v,arg(e,1),arg(e,0),res)) return res;
}
if((!truth && op(e) == And) || (truth && op(e) == Or)){
int nargs = num_args(e);
for(int i = 0; i < nargs; i++){
ast res = cont_eq(cont_eq_memo, truth, v, arg(e,i));
if(!res.null()) return res;
}
}
if(truth && op(e) == Implies){
ast res = cont_eq(cont_eq_memo, !truth, v, arg(e,0));
if(!res.null()) return res;
res = cont_eq(cont_eq_memo, truth, v, arg(e,1));
if(!res.null()) return res;
}
return ast();
}
// substitute a term t for unbound occurrences of variable v in e
iz3mgr::ast iz3mgr::subst(stl_ext::hash_map<ast,ast> &subst_memo, ast var, ast t, ast e){
if(e == var) return t;
std::pair<ast,ast> foo(e,ast());
std::pair<hash_map<ast,ast>::iterator,bool> bar = subst_memo.insert(foo);
ast &res = bar.first->second;
if(bar.second){
int nargs = num_args(e);
std::vector<ast> args(nargs);
for(int i = 0; i < nargs; i++)
args[i] = subst(subst_memo,var,t,arg(e,i));
opr f = op(e);
if(f == Equal && args[0] == args[1]) res = mk_true();
else res = clone(e,args);
}
return res;
}
iz3mgr::ast iz3mgr::subst(ast var, ast t, ast e){
hash_map<ast,ast> memo;
return subst(memo,var,t,e);
}
iz3mgr::ast iz3mgr::subst(stl_ext::hash_map<ast,ast> &subst_memo,ast e){
std::pair<ast,ast> foo(e,ast());
std::pair<hash_map<ast,ast>::iterator,bool> bar = subst_memo.insert(foo);
ast &res = bar.first->second;
if(bar.second){
int nargs = num_args(e);
std::vector<ast> args(nargs);
for(int i = 0; i < nargs; i++)
args[i] = subst(subst_memo,arg(e,i));
opr f = op(e);
if(f == Equal && args[0] == args[1]) res = mk_true();
else res = clone(e,args);
}
return res;
}
// apply a quantifier to a formula, with some optimizations
// 1) bound variable does not occur -> no quantifier
// 2) bound variable must be equal to some term -> substitute
iz3mgr::ast iz3mgr::apply_quant(opr quantifier, ast var, ast e){
if((quantifier == Forall && op(e) == And)
|| (quantifier == Exists && op(e) == Or)){
int n = num_args(e);
std::vector<ast> args(n);
for(int i = 0; i < n; i++)
args[i] = apply_quant(quantifier,var,arg(e,i));
return make(op(e),args);
}
if(!occurs_in(var,e))return e;
hash_set<ast> cont_eq_memo;
ast cterm = cont_eq(cont_eq_memo, quantifier == Forall, var, e);
if(!cterm.null()){
return subst(var,cterm,e);
}
std::vector<ast> bvs; bvs.push_back(var);
return make_quant(quantifier,bvs,e);
}
#if 0
void iz3mgr::get_bound_substitutes(stl_ext::hash_map<ast,bool> &memo, const ast &e, const ast &var, std::vector<ast> &substs){
std::pair<ast,bool> foo(e,false);
std::pair<hash_map<ast,bool>::iterator,bool> bar = memo.insert(foo);
if(bar.second){
if(op(e) ==
}
}
#endif
unsigned iz3mgr::num_free_variables(const ast &e){
used_vars uv;
uv(to_expr(e.raw()));
return uv.get_num_vars();
}
iz3mgr::ast iz3mgr::close_universally (ast e){
used_vars uv;
uv(to_expr(e.raw()));
std::vector<ast> bvs;
stl_ext::hash_map<ast,ast> subst_memo;
for (unsigned i = 0; i < uv.get_max_found_var_idx_plus_1(); i++){
if (uv.get(i)) {
std::ostringstream os;
os << "%%" << i;
ast c = make_var(os.str(),uv.get(i));
ast v = cook(m().mk_var(i,uv.get(i)));
subst_memo[v] = c;
bvs.push_back(c);
}
}
e = subst(subst_memo,e);
for (unsigned i = 0; i < bvs.size(); i++)
e = apply_quant(Forall,bvs[i],e);
return e;
}

738
src/interp/iz3mgr.h
View file

@ -1,738 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
iz3mgr.h
Abstract:
A wrapper around an ast manager, providing convenience methods.
Author:
Ken McMillan (kenmcmil)
Revision History:
--*/
#ifndef IZ3MGR_H
#define IZ3MGR_H
#include <assert.h>
#include <vector>
#include <functional>
#include "interp/iz3hash.h"
#include "interp/iz3exception.h"
#include "ast/well_sorted.h"
#include "ast/arith_decl_plugin.h"
#include "ast/bv_decl_plugin.h"
#include "ast/datatype_decl_plugin.h"
#include "ast/array_decl_plugin.h"
#include "ast/ast_translation.h"
#include "ast/ast_pp.h"
#include "ast/ast_ll_pp.h"
#include "ast/ast_smt_pp.h"
#include "ast/ast_smt2_pp.h"
#include "ast/rewriter/th_rewriter.h"
#include "ast/rewriter/var_subst.h"
#include "ast/expr_substitution.h"
#include "ast/pp.h"
#include "util/scoped_ctrl_c.h"
#include "util/cancel_eh.h"
#include "util/scoped_timer.h"
/* A wrapper around an ast manager, providing convenience methods. */
/** Shorthands for some built-in operators. */
// rename this to keep it accessible, as we use ast for something else
typedef ast raw_ast;
/** Wrapper around an ast pointer */
class ast_i {
protected:
raw_ast *_ast;
public:
raw_ast * const &raw() const {return _ast;}
ast_i(raw_ast *a){_ast = a;}
ast_i(){_ast = nullptr;}
bool eq(const ast_i &other) const {
return _ast == other._ast;
}
bool lt(const ast_i &other) const {
return _ast->get_id() < other._ast->get_id();
}
friend bool operator==(const ast_i &x, const ast_i&y){
return x.eq(y);
}
friend bool operator!=(const ast_i &x, const ast_i&y){
return !x.eq(y);
}
friend bool operator<(const ast_i &x, const ast_i&y){
return x.lt(y);
}
size_t hash() const {return _ast->get_id();}
bool null() const {return !_ast;}
};
/** Reference counting verison of above */
class ast_r : public ast_i {
ast_manager *_m;
public:
ast_r(ast_manager *m, raw_ast *a) : ast_i(a) {
_m = m;
m->inc_ref(a);
}
ast_r() {_m = nullptr;}
ast_r(const ast_r &other) : ast_i(other) {
_m = other._m;
if (_m) _m->inc_ref(_ast);
}
ast_r &operator=(const ast_r &other) {
if(_ast)
_m->dec_ref(_ast);
_ast = other._ast;
_m = other._m;
if (_m) _m->inc_ref(_ast);
return *this;
}
~ast_r() {
if(_ast)
_m->dec_ref(_ast);
}
ast_manager *mgr() const {return _m;}
};
// to make ast_r hashable
namespace hash_space {
template <>
class hash<ast_r> {
public:
size_t operator()(const ast_r &s) const {
return s.raw()->get_id();
}
};
}
// to make ast_r usable in ordered collections
namespace std {
template <>
class less<ast_r> {
public:
bool operator()(const ast_r &s, const ast_r &t) const {
// return s.raw() < t.raw();
return s.raw()->get_id() < t.raw()->get_id();
}
};
}
/** Wrapper around an AST manager, providing convenience methods. */
class iz3mgr {
public:
typedef ast_r ast;
// typedef decl_kind opr;
typedef func_decl *symb;
typedef sort *type;
typedef ast_r z3pf;
typedef decl_kind pfrule;
enum opr {
True,
False,
And,
Or,
Not,
Iff,
Ite,
Equal,
Implies,
Distinct,
Xor,
Oeq,
Interp,
Leq,
Geq,
Lt,
Gt,
Plus,
Sub,
Uminus,
Times,
Div,
Idiv,
Rem,
Mod,
Power,
ToReal,
ToInt,
IsInt,
Select,
Store,
ConstArray,
ArrayDefault,
ArrayMap,
SetUnion,
SetIntersect,
SetDifference,
SetComplement,
SetSubSet,
AsArray,
Numeral,
Forall,
Exists,
Variable,
Uninterpreted,
Other
};
opr op(const ast &t);
unsigned ast_id(const ast &x)
{
return to_expr(x.raw())->get_id();
}
/** Overloads for constructing ast. */
ast make_var(const std::string &name, type ty);
ast make(opr op, const std::vector<ast> &args);
ast make(opr op);
ast make(opr op, const ast &arg0);
ast make(opr op, const ast &arg0, const ast &arg1);
ast make(opr op, const ast &arg0, const ast &arg1, const ast &arg2);
ast make(symb sym, const std::vector<ast> &args);
ast make(symb sym);
ast make(symb sym, const ast &arg0);
ast make(symb sym, const ast &arg0, const ast &arg1);
ast make(symb sym, const ast &arg0, const ast &arg1, const ast &arg2);
ast make_quant(opr op, const std::vector<ast> &bvs, ast &body);
ast clone(const ast &t, const std::vector<ast> &args);
ast_manager &m() {return m_manager;}
ast cook(raw_ast *a) {return ast(&m_manager,a);}
std::vector<ast> cook(ptr_vector<raw_ast> v) {
std::vector<ast> _v(v.size());
for(unsigned i = 0; i < v.size(); i++)
_v[i] = cook(v[i]);
return _v;
}
raw_ast *uncook(const ast &a) {
m_manager.inc_ref(a.raw());
return a.raw();
}
/** Methods for destructing ast. */
int num_args(const ast& t){
ast_kind dk = t.raw()->get_kind();
switch(dk){
case AST_APP:
return to_app(t.raw())->get_num_args();
case AST_QUANTIFIER:
return 1;
case AST_VAR:
return 0;
default:;
}
assert(0);
return 0;
}
ast arg(const ast &t, int i){
ast_kind dk = t.raw()->get_kind();
switch(dk){
case AST_APP:
return cook(to_app(t.raw())->get_arg(i));
case AST_QUANTIFIER:
return cook(to_quantifier(t.raw())->get_expr());
default:;
}
assert(0);
return ast();
}
void get_args(const ast &t, std::vector<ast> &res){
res.resize(num_args(t));
for(unsigned i = 0; i < res.size(); i++)
res[i] = arg(t,i);
}
std::vector<ast> args(const ast &t){
std::vector<ast> res;
get_args(t,res);
return res;
}
symb sym(const ast& t){
raw_ast *_ast = t.raw();
return is_app(_ast) ? to_app(_ast)->get_decl() : nullptr;
}
std::string string_of_symbol(symb s){
symbol _s = s->get_name();
if (_s.is_numerical()) {
std::ostringstream buffer;
buffer << _s.get_num();
return buffer.str();
}
else {
return _s.bare_str();
}
}
type get_type(const ast& t){
return m().get_sort(to_expr(t.raw()));
}
std::string string_of_numeral(const ast& t){
rational r;
expr* e = to_expr(t.raw());
assert(e);
if (m_arith_util.is_numeral(e, r))
return r.to_string();
assert(0);
return "NaN";
}
bool is_numeral(const ast& t, rational &r){
expr* e = to_expr(t.raw());
assert(e);
return m_arith_util.is_numeral(e, r);
}
rational get_coeff(const ast& t){
rational res;
if(op(t) == Times && is_numeral(arg(t,0),res))
return res;
return rational(1);
}
ast get_linear_var(const ast& t){
rational res;
if(op(t) == Times && is_numeral(arg(t,0),res))
return arg(t,1);
return t;
}
int get_quantifier_num_bound(const ast &t) {
return to_quantifier(t.raw())->get_num_decls();
}
std::string get_quantifier_bound_name(const ast &t, unsigned i) {
return to_quantifier(t.raw())->get_decl_names()[i].bare_str();
}
type get_quantifier_bound_type(const ast &t, unsigned i) {
return to_quantifier(t.raw())->get_decl_sort(i);
}
ast get_quantifier_body(const ast &t) {
return cook(to_quantifier(t.raw())->get_expr());
}
unsigned get_variable_index_value(const ast &t) {
var* va = to_var(t.raw());
return va->get_idx();
}
bool is_bool_type(type t){
family_id fid = to_sort(t)->get_family_id();
decl_kind k = to_sort(t)->get_decl_kind();
return fid == m().get_basic_family_id() && k == BOOL_SORT;
}
bool is_array_type(type t){
family_id fid = to_sort(t)->get_family_id();
decl_kind k = to_sort(t)->get_decl_kind();
return fid == m_array_fid && k == ARRAY_SORT;
}
type get_range_type(symb s){
return to_func_decl(s)->get_range();
}
int get_num_parameters(const symb &s){
return to_func_decl(s)->get_num_parameters();
}
ast get_ast_parameter(const symb &s, int idx){
return cook(to_func_decl(s)->get_parameters()[idx].get_ast());
}
enum lemma_theory {ArithTheory,ArrayTheory,UnknownTheory};
lemma_theory get_theory_lemma_theory(const ast &proof){
symb s = sym(proof);
::symbol p0;
bool ok = s->get_parameter(0).is_symbol(p0);
if(!ok) return UnknownTheory;
std::string foo(p0.bare_str());
if(foo == "arith")
return ArithTheory;
if(foo == "array")
return ArrayTheory;
return UnknownTheory;
}
enum lemma_kind {FarkasKind,Leq2EqKind,Eq2LeqKind,GCDTestKind,AssignBoundsKind,EqPropagateKind,GomoryCutKind,ArithMysteryKind,UnknownKind};
lemma_kind get_theory_lemma_kind(const ast &proof){
symb s = sym(proof);
if(s->get_num_parameters() < 2) {
return ArithMysteryKind; // Bad -- Z3 hasn't told us
}
::symbol p0;
bool ok = s->get_parameter(1).is_symbol(p0);
if(!ok) return UnknownKind;
std::string foo(p0.bare_str());
if(foo == "farkas")
return FarkasKind;
if(foo == "triangle-eq")
return is_not(arg(conc(proof),0)) ? Eq2LeqKind : Leq2EqKind;
if(foo == "gcd-test")
return GCDTestKind;
if(foo == "assign-bounds")
return AssignBoundsKind;
if(foo == "eq-propagate")
return EqPropagateKind;
if(foo == "gomory-cut")
return GomoryCutKind;
return UnknownKind;
}
void get_farkas_coeffs(const ast &proof, std::vector<ast>& coeffs);
void get_farkas_coeffs(const ast &proof, std::vector<rational>& rats);
void get_broken_gcd_test_coeffs(const ast &proof, std::vector<rational>& rats);
void get_assign_bounds_coeffs(const ast &proof, std::vector<rational>& rats);
void get_assign_bounds_coeffs(const ast &proof, std::vector<ast>& rats);
void get_assign_bounds_rule_coeffs(const ast &proof, std::vector<rational>& rats);
void get_assign_bounds_rule_coeffs(const ast &proof, std::vector<ast>& rats);
void get_gomory_cut_coeffs(const ast &proof, std::vector<rational>& rats);
void get_gomory_cut_coeffs(const ast &proof, std::vector<ast>& rats);
bool is_farkas_coefficient_negative(const ast &proof, int n);
bool is_true(const ast& t){
return op(t) == True;
}
bool is_false(const ast& t){
return op(t) == False;
}
bool is_iff(const ast& t){
return op(t) == Iff;
}
bool is_or(const ast& t){
return op(t) == Or;
}
bool is_not(const ast& t){
return op(t) == Not;
}
/** Simplify an expression using z3 simplifier */
ast z3_simplify(const ast& e);
/** Simplify, sorting sums */
ast z3_really_simplify(const ast &e);
// Some constructors that simplify things
ast mk_not(const ast& x){
opr o = op(x);
if(o == True) return make(False);
if(o == False) return make(True);
if(o == Not) return arg(x,0);
return make(Not,x);
}
ast mk_and(const ast& x, const ast& y){
opr ox = op(x);
opr oy = op(y);
if(ox == True) return y;
if(oy == True) return x;
if(ox == False) return x;
if(oy == False) return y;
if(x == y) return x;
return make(And,x,y);
}
ast mk_or(const ast& x, const ast& y){
opr ox = op(x);
opr oy = op(y);
if(ox == False) return y;
if(oy == False) return x;
if(ox == True) return x;
if(oy == True) return y;
if(x == y) return x;
return make(Or,x,y);
}
ast mk_implies(const ast& x, const ast& y){
opr ox = op(x);
opr oy = op(y);
if(ox == True) return y;
if(oy == False) return mk_not(x);
if(ox == False) return mk_true();
if(oy == True) return y;
if(x == y) return mk_true();
return make(Implies,x,y);
}
ast mk_or(const std::vector<ast> &x){
ast res = mk_false();
for(unsigned i = 0; i < x.size(); i++)
res = mk_or(res,x[i]);
return res;
}
ast mk_and(const std::vector<ast> &x){
std::vector<ast> conjs;
for(unsigned i = 0; i < x.size(); i++){
const ast &e = x[i];
opr o = op(e);
if(o == False)
return mk_false();
if(o != True)
conjs.push_back(e);
}
if(conjs.size() == 0)
return mk_true();
if(conjs.size() == 1)
return conjs[0];
return make(And,conjs);
}
ast mk_equal(const ast& x, const ast& y){
if(x == y) return make(True);
opr ox = op(x);
opr oy = op(y);
if(ox == True) return y;
if(oy == True) return x;
if(ox == False) return mk_not(y);
if(oy == False) return mk_not(x);
if(ox == False && oy == True) return make(False);
if(oy == False && ox == True) return make(False);
return make(Equal,x,y);
}
ast z3_ite(const ast& x, const ast& y, const ast& z){
opr ox = op(x);
opr oy = op(y);
opr oz = op(z);
if(ox == True) return y;
if(ox == False) return z;
if(y == z) return y;
if(oy == True && oz == False) return x;
if(oz == True && oy == False) return mk_not(x);
return make(Ite,x,y,z);
}
ast make_int(const std::string &s) {
sort *r = m().mk_sort(m_arith_fid, INT_SORT);
return cook(m_arith_util.mk_numeral(rational(s.c_str()),r));
}
ast make_int(const rational &s) {
sort *r = m().mk_sort(m_arith_fid, INT_SORT);
return cook(m_arith_util.mk_numeral(s,r));
}
ast make_real(const std::string &s) {
sort *r = m().mk_sort(m_arith_fid, REAL_SORT);
return cook(m_arith_util.mk_numeral(rational(s.c_str()),r));
}
ast make_real(const rational &s) {
sort *r = m().mk_sort(m_arith_fid, REAL_SORT);
return cook(m_arith_util.mk_numeral(s,r));
}
ast mk_false() { return make(False); }
ast mk_true() { return make(True); }
ast mk_fresh_constant(char const * prefix, type s){
return cook(m().mk_fresh_const(prefix, s));
}
type bool_type() {
::sort *s = m().mk_sort(m_basic_fid, BOOL_SORT);
return s;
}
type int_type() {
::sort *s = m().mk_sort(m_arith_fid, INT_SORT);
return s;
}
type real_type() {
::sort *s = m().mk_sort(m_arith_fid, REAL_SORT);
return s;
}
type array_type(type d, type r) {
parameter params[2] = { parameter(d), parameter(to_sort(r)) };
::sort * s = m().mk_sort(m_array_fid, ARRAY_SORT, 2, params);
return s;
}
symb function(const std::string &str_name, unsigned arity, type *domain, type range) {
::symbol name = ::symbol(str_name.c_str());
std::vector< ::sort *> sv(arity);
for(unsigned i = 0; i < arity; i++)
sv[i] = domain[i];
::func_decl* d = m().mk_func_decl(name,arity,&sv[0],range);
return d;
}
void linear_comb(ast &P, const ast &c, const ast &Q, bool round_off = false);
ast sum_inequalities(const std::vector<ast> &coeffs, const std::vector<ast> &ineqs, bool round_off = false);
ast simplify_ineq(const ast &ineq){
ast res = make(op(ineq),arg(ineq,0),z3_simplify(arg(ineq,1)));
return res;
}
void mk_idiv(const ast& t, const rational &d, ast &whole, ast &frac);
ast mk_idiv(const ast& t, const rational &d);
ast mk_idiv(const ast& t, const ast &d);
/** methods for destructing proof terms */
pfrule pr(const z3pf &t);
int num_prems(const z3pf &t){return to_app(t.raw())->get_num_args()-1;}
z3pf prem(const z3pf &t, int n){return arg(t,n);}
z3pf conc(const z3pf &t){return arg(t,num_prems(t));}
/* quantifier handling */
// substitute a term t for unbound occurrences of variable v in e
ast subst(ast var, ast t, ast e);
// apply a substitution defined by a map
ast subst(stl_ext::hash_map<ast,ast> &map, ast e);
// apply a quantifier to a formula, with some optimizations
// 1) bound variable does not occur -> no quantifier
// 2) bound variable must be equal to some term -> substitute
ast apply_quant(opr quantifier, ast var, ast e);
// Universally quantify all the free variables in a formula.
// Makes up names for the quntifiers.
ast close_universally (ast e);
unsigned num_free_variables(const ast &e);
/** For debugging */
void show(ast);
void show_symb(symb s);
/** Constructor */
void print_lit(ast lit);
void print_expr(std::ostream &s, const ast &e);
void print_clause(std::ostream &s, std::vector<ast> &cls);
void print_sat_problem(std::ostream &out, const ast &t);
void show_clause(std::vector<ast> &cls);
static void pretty_print(std::ostream &f, const std::string &s);
iz3mgr(ast_manager &_m_manager)
: m_manager(_m_manager),
m_arith_util(_m_manager)
{
m_basic_fid = m().get_basic_family_id();
m_arith_fid = m().mk_family_id("arith");
m_bv_fid = m().mk_family_id("bv");
m_array_fid = m().mk_family_id("array");
m_dt_fid = m().mk_family_id("datatype");
m_datalog_fid = m().mk_family_id("datalog_relation");
}
iz3mgr(const iz3mgr& other)
: m_manager(other.m_manager),
m_arith_util(other.m_manager)
{
m_basic_fid = m().get_basic_family_id();
m_arith_fid = m().mk_family_id("arith");
m_bv_fid = m().mk_family_id("bv");
m_array_fid = m().mk_family_id("array");
m_dt_fid = m().mk_family_id("datatype");
m_datalog_fid = m().mk_family_id("datalog_relation");
}
protected:
ast_manager &m_manager;
int occurs_in(ast var, ast e);
private:
ast mki(family_id fid, decl_kind sk, int n, raw_ast **args);
ast make(opr op, int n, raw_ast **args);
ast make(symb sym, int n, raw_ast **args);
int occurs_in1(stl_ext::hash_map<ast,bool> &occurs_in_memo, ast var, ast e);
bool solve_arith(const ast &v, const ast &x, const ast &y, ast &res);
ast cont_eq(stl_ext::hash_set<ast> &cont_eq_memo, bool truth, ast v, ast e);
ast subst(stl_ext::hash_map<ast,ast> &subst_memo, ast var, ast t, ast e);
family_id m_basic_fid;
family_id m_array_fid;
family_id m_arith_fid;
family_id m_bv_fid;
family_id m_dt_fid;
family_id m_datalog_fid;
arith_util m_arith_util;
};
#endif

185
src/interp/iz3pp.cpp
View file

@ -1,185 +0,0 @@
/*++
Copyright (c) 2013 Microsoft Corporation
Module Name:
iz3pp.cpp
Abstract:
Pretty-print interpolation problems
Author:
Ken McMillan (kenmcmil)
Revision History:
--*/
/* Copyright 2011 Microsoft Research. */
#include <assert.h>
#include <algorithm>
#include <stdio.h>
#include <fstream>
#include <sstream>
#include <set>
#include <iostream>
#include "interp/iz3mgr.h"
#include "interp/iz3pp.h"
#include "ast/func_decl_dependencies.h"
#include "ast/for_each_expr.h"
#include "ast/ast_smt_pp.h"
#include "ast/ast_smt2_pp.h"
#include "ast/expr_functors.h"
#include "ast/expr_abstract.h"
using namespace stl_ext;
// We promise not to use this for hash_map with range destructor
namespace stl_ext {
template <>
class hash<expr *> {
public:
size_t operator()(const expr *p) const {
return (size_t) p;
}
};
}
// TBD: algebraic data-types declarations will not be printed.
class free_func_visitor {
ast_manager& m;
func_decl_set m_funcs;
obj_hashtable<class sort> m_sorts;
public:
free_func_visitor(ast_manager& m): m(m) {}
void operator()(var * n) { }
void operator()(app * n) {
m_funcs.insert(n->get_decl());
class sort* s = m.get_sort(n);
if (s->get_family_id() == null_family_id) {
m_sorts.insert(s);
}
}
void operator()(quantifier * n) { }
func_decl_set& funcs() { return m_funcs; }
obj_hashtable<class sort>& sorts() { return m_sorts; }
};
class iz3pp_helper : public iz3mgr {
public:
void print_tree(const ast &tree, hash_map<expr*,symbol> &cnames, std::ostream &out){
hash_map<expr*,symbol>::iterator foo = cnames.find(to_expr(tree.raw()));
if(foo != cnames.end()){
symbol nm = foo->second;
if (is_smt2_quoted_symbol(nm)) {
out << mk_smt2_quoted_symbol(nm);
}
else {
out << nm;
}
}
else if(op(tree) == And){
out << "(and";
int nargs = num_args(tree);
for(int i = 0; i < nargs; i++){
out << " ";
print_tree(arg(tree,i), cnames, out);
}
out << ")";
}
else if(op(tree) == Interp){
out << "(interp ";
print_tree(arg(tree,0), cnames, out);
out << ")";
}
else throw iz3pp_bad_tree();
}
iz3pp_helper(ast_manager &_m_manager)
: iz3mgr(_m_manager) {}
};
void iz3pp(ast_manager &m,
const ptr_vector<expr> &cnsts_vec,
expr *tree,
std::ostream& out) {
unsigned sz = cnsts_vec.size();
expr* const* cnsts = &cnsts_vec[0];
out << "(set-option :produce-interpolants true)\n";
free_func_visitor visitor(m);
expr_mark visited;
bool print_low_level = true; // m_params.print_low_level_smt2();
#define PP(_e_) if (print_low_level) out << mk_smt_pp(_e_, m); else ast_smt2_pp(out, _e_, env);
smt2_pp_environment_dbg env(m);
for (unsigned i = 0; i < sz; ++i) {
expr* e = cnsts[i];
for_each_expr(visitor, visited, e);
}
// name all the constraints
hash_map<expr *, symbol> cnames;
int ctr = 1;
for(unsigned i = 0; i < sz; i++){
symbol nm;
std::ostringstream s;
s << "f!" << (ctr++);
cnames[cnsts[i]] = symbol(s.str().c_str());
}
func_decl_set &funcs = visitor.funcs();
func_decl_set::iterator it = funcs.begin(), end = funcs.end();
obj_hashtable<class sort>& sorts = visitor.sorts();
obj_hashtable<class sort>::iterator sit = sorts.begin(), send = sorts.end();
for (; sit != send; ++sit) {
PP(*sit);
}
for (; it != end; ++it) {
func_decl* f = *it;
if(f->get_family_id() == null_family_id){
PP(f);
out << "\n";
}
}
for (unsigned i = 0; i < sz; ++i) {
out << "(assert ";
expr* r = cnsts[i];
symbol nm = cnames[r];
out << "(! ";
PP(r);
out << " :named ";
if (is_smt2_quoted_symbol(nm)) {
out << mk_smt2_quoted_symbol(nm);
}
else {
out << nm;
}
out << ")";
out << ")\n";
}
out << "(check-sat)\n";
out << "(get-interpolant ";
iz3pp_helper pp(m);
pp.print_tree(pp.cook(tree),cnames,out);
out << ")\n";
}

36
src/interp/iz3pp.h
View file

@ -1,36 +0,0 @@
/*++
Copyright (c) 2013 Microsoft Corporation
Module Name:
iz3pp.cpp
Abstract:
Pretty-print interpolation problems
Author:
Ken McMillan (kenmcmil)
Revision History:
--*/
#ifndef IZ3_PP_H
#define IZ3_PP_H
#include "interp/iz3mgr.h"
/** Exception thrown in case of mal-formed tree interpoloation
specification */
struct iz3pp_bad_tree: public iz3_exception {
iz3pp_bad_tree(): iz3_exception("iz3pp_bad_tree") {}
};
void iz3pp(ast_manager &m,
const ptr_vector<expr> &cnsts_vec,
expr *tree,
std::ostream& out);
#endif

153
src/interp/iz3profiling.cpp
View file

@ -1,153 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
iz3profiling.h
Abstract:
Some routines for measuring performance.
Author:
Ken McMillan (kenmcmil)
Revision History:
--*/
#ifdef _WINDOWS
#pragma warning(disable:4996)
#pragma warning(disable:4800)
#pragma warning(disable:4267)
#pragma warning(disable:4101)
#endif
#include "interp/iz3profiling.h"
#include <map>
#include <iostream>
#include <string>
#include <string.h>
#include <stdlib.h>
#include "util/stopwatch.h"
// FIXME fill in these stubs
#define clock_t double
static double current_time()
{
static stopwatch sw;
static bool started = false;
if(!started){
sw.start();
started = true;
}
return sw.get_current_seconds();
}
static void output_time(std::ostream &os, clock_t time){
os << time;
}
namespace profiling {
void show_time(){
output_time(std::cout,current_time());
std::cout << "\n";
}
typedef std::map<const char*, struct node> nmap;
struct node {
std::string name;
clock_t time;
clock_t start_time;
nmap sub;
struct node *parent;
node();
} top;
node::node(){
time = 0;
parent = nullptr;
}
struct node *current;
struct init {
init(){
top.name = "TOTAL";
current = &top;
}
} initializer;
struct time_entry {
clock_t t;
time_entry(){t = 0;};
void add(clock_t incr){t += incr;}
};
struct ltstr
{
bool operator()(const char* s1, const char* s2) const
{
return strcmp(s1, s2) < 0;
}
};
typedef std::map<const char*, time_entry, ltstr> tmap;
static std::ostream *pfs;
void print_node(node &top, int indent, tmap &totals){
for(int i = 0; i < indent; i++) (*pfs) << " ";
(*pfs) << top.name;
int dots = 70 - 2 * indent - top.name.size();
for(int i = 0; i <dots; i++) (*pfs) << ".";
output_time(*pfs, top.time);
(*pfs) << std::endl;
if(indent != 0)totals[top.name.c_str()].add(top.time);
for(nmap::iterator it = top.sub.begin(); it != top.sub.end(); it++)
print_node(it->second,indent+1,totals);
}
void print(std::ostream &os) {
pfs = &os;
top.time = 0;
for(nmap::iterator it = top.sub.begin(); it != top.sub.end(); it++)
top.time += it->second.time;
tmap totals;
print_node(top,0,totals);
(*pfs) << "TOTALS:" << std::endl;
for(tmap::iterator it = totals.begin(); it != totals.end(); it++){
(*pfs) << (it->first) << " ";
output_time(*pfs, it->second.t);
(*pfs) << std::endl;
}
}
void timer_start(const char *name){
node &child = current->sub[name];
if(child.name.empty()){ // a new node
child.parent = current;
child.name = name;
}
child.start_time = current_time();
current = &child;
}
void timer_stop(const char *name){
if(current->name != name || !current->parent){
std::cerr << "imbalanced timer_start and timer_stop";
exit(1);
}
current->time += (current_time() - current->start_time);
current = current->parent;
}
}

37
src/interp/iz3profiling.h
View file

@ -1,37 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
iz3profiling.h
Abstract:
Some routines for measuring performance.
Author:
Ken McMillan (kenmcmil)
Revision History:
--*/
#ifndef IZ3PROFILING_H
#define IZ3PROFILING_H
#include <ostream>
namespace profiling {
/** Start a timer with given name */
void timer_start(const char *);
/** Stop a timer with given name */
void timer_stop(const char *);
/** Print out timings */
void print(std::ostream &s);
/** Show the current time. */
void show_time();
}
#endif

628
src/interp/iz3proof.cpp
View file

@ -1,628 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
iz3proof.cpp
Abstract:
This class defines a simple interpolating proof system.
Author:
Ken McMillan (kenmcmil)
Revision History:
--*/
#ifdef _WINDOWS
#pragma warning(disable:4996)
#pragma warning(disable:4800)
#pragma warning(disable:4267)
#pragma warning(disable:4101)
#endif
#include "interp/iz3proof.h"
#include "interp/iz3profiling.h"
#include<algorithm>
#include <iterator>
#include <iostream>
#include <sstream>
// #define FACTOR_INTERPS
// #define CHECK_PROOFS
void iz3proof::resolve(ast pivot, std::vector<ast> &cls1, const std::vector<ast> &cls2){
#ifdef CHECK_PROOFS
std::vector<ast> orig_cls1 = cls1;
#endif
ast neg_pivot = pv->mk_not(pivot);
bool found_pivot1 = false, found_pivot2 = false;
for(unsigned i = 0; i < cls1.size(); i++){
if(cls1[i] == neg_pivot){
cls1[i] = cls1.back();
cls1.pop_back();
found_pivot1 = true;
break;
}
}
{
std::set<ast> memo;
memo.insert(cls1.begin(),cls1.end());
for(unsigned j = 0; j < cls2.size(); j++){
if(cls2[j] == pivot)
found_pivot2 = true;
else
if(memo.find(cls2[j]) == memo.end())
cls1.push_back(cls2[j]);
}
}
if(found_pivot1 && found_pivot2)
return;
#ifdef CHECK_PROOFS
std::cerr << "resolution anomaly: " << nodes.size()-1 << "\n";
#if 0
std::cerr << "pivot: "; {pv->print_lit(pivot); std::cout << "\n";}
std::cerr << "left clause:\n";
for(unsigned i = 0; i < orig_cls1.size(); i++)
{pv->print_lit(orig_cls1[i]); std::cout << "\n";}
std::cerr << "right clause:\n";
for(unsigned i = 0; i < cls2.size(); i++)
{pv->print_lit(cls2[i]); std::cout << "\n";}
throw proof_error();
#endif
#endif
}
iz3proof::node iz3proof::make_resolution(ast pivot, node premise1, node premise2)
{
if(nodes[premise1].rl == Hypothesis) return premise2; // resolve with hyp is noop
if(nodes[premise2].rl == Hypothesis) return premise1;
node res = make_node();
node_struct &n = nodes[res];
n.rl = Resolution;
n.aux = pivot;
n.premises.resize(2);
n.premises[0] = (premise1);
n.premises[1] = (premise2);
#ifdef CHECK_PROOFS
n.conclusion = nodes[premise1].conclusion;
resolve(pivot,n.conclusion,nodes[premise2].conclusion);
n.frame = 1;
#else
n.frame = 0; // compute conclusion lazily
#endif
return res;
}
iz3proof::node iz3proof::resolve_lemmas(ast pivot, node premise1, node premise2)
{
std::vector<ast> lits(nodes[premise1].conclusion), itp; // no interpolant
resolve(pivot,lits,nodes[premise2].conclusion);
return make_lemma(lits,itp);
}
iz3proof::node iz3proof::make_assumption(int frame, const std::vector<ast> &assumption){
#if 0
std::cout << "assumption: \n";
for(unsigned i = 0; i < assumption.size(); i++)
pv->show(assumption[i]);
std::cout << "\n";
#endif
node res = make_node();
node_struct &n = nodes[res];
n.rl = Assumption;
n.conclusion.resize(1);
n.conclusion = assumption;
n.frame = frame;
return res;
}
iz3proof::node iz3proof::make_hypothesis(ast hypothesis){
node res = make_node();
node_struct &n = nodes[res];
n.rl = Hypothesis;
n.conclusion.resize(2);
n.conclusion[0] = hypothesis;
n.conclusion[1] = pv->mk_not(hypothesis);
return res;
}
iz3proof::node iz3proof::make_theory(const std::vector<ast> &conclusion, std::vector<node> premises){
node res = make_node();
node_struct &n = nodes[res];
n.rl = Theory;
n.conclusion = conclusion;
n.premises = premises;
return res;
}
iz3proof::node iz3proof::make_axiom(const std::vector<ast> &conclusion){
node res = make_node();
node_struct &n = nodes[res];
n.rl = Axiom;
n.conclusion = conclusion;
return res;
}
iz3proof::node iz3proof::make_contra(node prem, const std::vector<ast> &conclusion){
node res = make_node();
node_struct &n = nodes[res];
n.rl = Contra;
n.conclusion = conclusion;
#ifdef CHECK_PROOFS
//if(!(conclusion == nodes[prem].conclusion)){
//std::cerr << "internal error: proof error\n";
//assert(0 && "proof error");
//}
#endif
n.premises.push_back(prem);
return res;
}
iz3proof::node iz3proof::make_lemma(const std::vector<ast> &conclusion, const std::vector<ast> &interpolation){
node res = make_node();
node_struct &n = nodes[res];
n.rl = Lemma;
n.conclusion = conclusion;
n.frame = interps.size();
interps.push_back(interpolation);
return res;
}
/** Make a Reflexivity node. This rule produces |- x = x */
iz3proof::node iz3proof::make_reflexivity(ast con){
node res = make_node();
node_struct &n = nodes[res];
n.rl = Reflexivity;
n.conclusion.push_back(con);
return res;
}
/** Make a Symmetry node. This takes a derivation of |- x = y and
produces | y = x */
iz3proof::node iz3proof::make_symmetry(ast con, node prem){
node res = make_node();
node_struct &n = nodes[res];
n.rl = Reflexivity;
n.conclusion.push_back(con);
n.premises.push_back(prem);
return res;
}
/** Make a transitivity node. This takes derivations of |- x = y
and |- y = z produces | x = z */
iz3proof::node iz3proof::make_transitivity(ast con, node prem1, node prem2){
node res = make_node();
node_struct &n = nodes[res];
n.rl = Transitivity;
n.conclusion.push_back(con);
n.premises.push_back(prem1);
n.premises.push_back(prem2);
return res;
}
/** Make a congruence node. This takes derivations of |- x_i = y_i
and produces |- f(x_1,...,x_n) = f(y_1,...,y_n) */
iz3proof::node iz3proof::make_congruence(ast con, const std::vector<node> &prems){
node res = make_node();
node_struct &n = nodes[res];
n.rl = Congruence;
n.conclusion.push_back(con);
n.premises = prems;
return res;
}
/** Make an equality contradicition node. This takes |- x = y
and |- !(x = y) and produces false. */
iz3proof::node iz3proof::make_eqcontra(node prem1, node prem2){
node res = make_node();
node_struct &n = nodes[res];
n.rl = EqContra;
n.premises.push_back(prem1);
n.premises.push_back(prem2);
return res;
}
iz3proof::node iz3proof::copy_rec(stl_ext::hash_map<node,node> &memo, iz3proof &src, node n){
stl_ext::hash_map<node,node>::iterator it = memo.find(n);
if(it != memo.end()) return (*it).second;
node_struct &ns = src.nodes[n];
std::vector<node> prems(ns.premises.size());
for(unsigned i = 0; i < prems.size(); i++)
prems[i] = copy_rec(memo,src,ns.premises[i]);
nodes.push_back(ns);
nodes.back().premises.swap(prems);
if(ns.rl == Lemma){
nodes.back().frame = interps.size();
interps.push_back(src.interps[ns.frame]);
}
int res = nodes.size()-1;
memo[n] = res;
return res;
}
iz3proof::node iz3proof::copy(iz3proof &src, node n){
stl_ext::hash_map<node,node> memo;
return copy_rec(memo, src, n);
}
bool iz3proof::pred_in_A(ast id){
return weak
? pv->ranges_intersect(pv->ast_range(id),rng) :
pv->range_contained(pv->ast_range(id),rng);
}
bool iz3proof::term_in_B(ast id){
prover::range r = pv->ast_scope(id);
if(weak) {
if(pv->range_min(r) == SHRT_MIN)
return !pv->range_contained(r,rng);
else
return !pv->ranges_intersect(r,rng);
}
else
return !pv->range_contained(r,rng);
}
bool iz3proof::frame_in_A(int frame){
return pv->in_range(frame,rng);
}
bool iz3proof::lit_in_B(ast lit){
return
b_lits.find(lit) != b_lits.end()
|| b_lits.find(pv->mk_not(lit)) != b_lits.end();
}
iz3proof::ast iz3proof::my_or(ast x, ast y){
return pv->mk_not(pv->mk_and(pv->mk_not(x),pv->mk_not(y)));
}
iz3proof::ast iz3proof::get_A_lits(std::vector<ast> &cls){
ast foo = pv->mk_false();
for(unsigned i = 0; i < cls.size(); i++){
ast lit = cls[i];
if(b_lits.find(pv->mk_not(lit)) == b_lits.end()){
if(pv->range_max(pv->ast_scope(lit)) == pv->range_min(pv->ast_scope(lit))){
std::cout << "bad lit: " << pv->range_max(rng) << " : " << pv->range_max(pv->ast_scope(lit)) << " : " << (pv->ast_id(lit)) << " : ";
pv->show(lit);
}
foo = my_or(foo,lit);
}
}
return foo;
}
iz3proof::ast iz3proof::get_B_lits(std::vector<ast> &cls){
ast foo = pv->mk_false();
for(unsigned i = 0; i < cls.size(); i++){
ast lit = cls[i];
if(b_lits.find(pv->mk_not(lit)) != b_lits.end())
foo = my_or(foo,lit);
}
return foo;
}
void iz3proof::set_of_B_lits(std::vector<ast> &cls, std::set<ast> &res){
for(unsigned i = 0; i < cls.size(); i++){
ast lit = cls[i];
if(b_lits.find(pv->mk_not(lit)) != b_lits.end())
res.insert(lit);
}
}
void iz3proof::set_of_A_lits(std::vector<ast> &cls, std::set<ast> &res){
for(unsigned i = 0; i < cls.size(); i++){
ast lit = cls[i];
if(b_lits.find(pv->mk_not(lit)) == b_lits.end())
res.insert(lit);
}
}
void iz3proof::find_B_lits(){
b_lits.clear();
for(unsigned i = 0; i < nodes.size(); i++){
node_struct &n = nodes[i];
std::vector<ast> &cls = n.conclusion;
if(n.rl == Assumption){
if(weak) goto lemma;
if(!frame_in_A(n.frame))
for(unsigned j = 0; j < cls.size(); j++)
b_lits.insert(cls[j]);
}
else if(n.rl == Lemma) {
lemma:
for(unsigned j = 0; j < cls.size(); j++)
if(term_in_B(cls[j]))
b_lits.insert(cls[j]);
}
}
}
iz3proof::ast iz3proof::disj_of_set(std::set<ast> &s){
ast res = pv->mk_false();
for(std::set<ast>::iterator it = s.begin(), en = s.end(); it != en; ++it)
res = my_or(*it,res);
return res;
}
void iz3proof::mk_and_factor(int p1, int p2, int i, std::vector<ast> &itps, std::vector<std::set<ast> > &disjs){
#ifdef FACTOR_INTERPS
std::set<ast> &d1 = disjs[p1];
std::set<ast> &d2 = disjs[p2];
if(!weak){
if(pv->is_true(itps[p1])){
itps[i] = itps[p2];
disjs[i] = disjs[p2];
}
else if(pv->is_true(itps[p2])){
itps[i] = itps[p1];
disjs[i] = disjs[p1];
}
else {
std::set<ast> p1only,p2only;
std::insert_iterator<std::set<ast> > p1o(p1only,p1only.begin());
std::insert_iterator<std::set<ast> > p2o(p2only,p2only.begin());
std::insert_iterator<std::set<ast> > dio(disjs[i],disjs[i].begin());
std::set_difference(d1.begin(),d1.end(),d2.begin(),d2.end(),p1o);
std::set_difference(d2.begin(),d2.end(),d1.begin(),d1.end(),p2o);
std::set_intersection(d1.begin(),d1.end(),d2.begin(),d2.end(),dio);
ast p1i = my_or(itps[p1],disj_of_set(p1only));
ast p2i = my_or(itps[p2],disj_of_set(p2only));
itps[i] = pv->mk_and(p1i,p2i);
}
}
else {
itps[i] = pv->mk_and(itps[p1],itps[p2]);
std::insert_iterator<std::set<ast> > dio(disjs[i],disjs[i].begin());
std::set_union(d1.begin(),d1.end(),d2.begin(),d2.end(),dio);
}
#endif
}
void iz3proof::mk_or_factor(int p1, int p2, int i, std::vector<ast> &itps, std::vector<std::set<ast> > &disjs){
#ifdef FACTOR_INTERPS
std::set<ast> &d1 = disjs[p1];
std::set<ast> &d2 = disjs[p2];
if(weak){
if(pv->is_false(itps[p1])){
itps[i] = itps[p2];
disjs[i] = disjs[p2];
}
else if(pv->is_false(itps[p2])){
itps[i] = itps[p1];
disjs[i] = disjs[p1];
}
else {
std::set<ast> p1only,p2only;
std::insert_iterator<std::set<ast> > p1o(p1only,p1only.begin());
std::insert_iterator<std::set<ast> > p2o(p2only,p2only.begin());
std::insert_iterator<std::set<ast> > dio(disjs[i],disjs[i].begin());
std::set_difference(d1.begin(),d1.end(),d2.begin(),d2.end(),p1o);
std::set_difference(d2.begin(),d2.end(),d1.begin(),d1.end(),p2o);
std::set_intersection(d1.begin(),d1.end(),d2.begin(),d2.end(),dio);
ast p1i = pv->mk_and(itps[p1],pv->mk_not(disj_of_set(p1only)));
ast p2i = pv->mk_and(itps[p2],pv->mk_not(disj_of_set(p2only)));
itps[i] = my_or(p1i,p2i);
}
}
else {
itps[i] = my_or(itps[p1],itps[p2]);
std::insert_iterator<std::set<ast> > dio(disjs[i],disjs[i].begin());
std::set_union(d1.begin(),d1.end(),d2.begin(),d2.end(),dio);
}
#endif
}
void iz3proof::interpolate_lemma(node_struct &n){
if(interps[n.frame].size())
return; // already computed
pv->interpolate_clause(n.conclusion,interps[n.frame]);
}
iz3proof::ast iz3proof::interpolate(const prover::range &_rng, bool _weak
#ifdef CHECK_PROOFS
, ast assump
, std::vector<int> *parents
#endif
){
// std::cout << "proof size: " << nodes.size() << "\n";
rng = _rng;
weak = _weak;
#ifdef CHECK_PROOFS
if(nodes[nodes.size()-1].conclusion.size() != 0)
std::cerr << "internal error: proof conclusion is not empty clause\n";
if(!child_interps.size()){
child_interps.resize(nodes.size());
for(unsigned j = 0; j < nodes.size(); j++)
child_interps[j] = pv->mk_true();
}
#endif
std::vector<ast> itps(nodes.size());
#ifdef FACTOR_INTERPS
std::vector<std::set<ast> > disjs(nodes.size());
#endif
profiling::timer_start("Blits");
find_B_lits();
profiling::timer_stop("Blits");
profiling::timer_start("interp_proof");
// strengthen();
for(unsigned i = 0; i < nodes.size(); i++){
node_struct &n = nodes[i];
ast &q = itps[i];
switch(n.rl){
case Assumption: {
if(frame_in_A(n.frame)){
/* HypC-A */
if(!weak)
#ifdef FACTOR_INTERPS
{
q = pv->mk_false();
set_of_B_lits(n.conclusion,disjs[i]);
}
#else
q = get_B_lits(n.conclusion);
#endif
else
q = pv->mk_false();
}
else {
/* HypEq-B */
if(!weak)
q = pv->mk_true();
else
#ifdef FACTOR_INTERPS
{
q = pv->mk_true();
set_of_A_lits(n.conclusion,disjs[i]);
}
#else
q = pv->mk_not(get_A_lits(n.conclusion));
#endif
}
break;
}
case Resolution: {
ast p = n.aux;
p = pv->is_not(p) ? pv->mk_not(p) : p; // should be positive, but just in case
if(lit_in_B(p))
#ifdef FACTOR_INTERPS
mk_and_factor(n.premises[0],n.premises[1],i,itps,disjs);
#else
q = pv->mk_and(itps[n.premises[0]],itps[n.premises[1]]);
#endif
else
#ifdef FACTOR_INTERPS
mk_or_factor(n.premises[0],n.premises[1],i,itps,disjs);
#else
q = my_or(itps[n.premises[0]],itps[n.premises[1]]);
#endif
break;
}
case Lemma: {
interpolate_lemma(n); // make sure lemma interpolants have been computed
q = interps[n.frame][pv->range_max(rng)];
break;
}
case Contra: {
q = itps[n.premises[0]];
#ifdef FACTOR_INTERPS
disjs[i] = disjs[n.premises[0]];
#endif
break;
}
default:
assert(0 && "rule not allowed in interpolated proof");
}
#ifdef CHECK_PROOFS
int this_frame = pv->range_max(rng);
if(0 && this_frame == 39) {
std::vector<ast> alits;
ast s = pv->mk_true();
for(unsigned j = 0; j < n.conclusion.size(); j++)
if(pred_in_A(n.conclusion[j])){
int scpmax = pv->range_max(pv->ast_scope(n.conclusion[j]));
if(scpmax == this_frame)
s = pv->mk_and(s,pv->mk_not(n.conclusion[j]));
}
ast ci = child_interps[i];
s = pv->mk_and(pv->mk_and(s,pv->mk_and(assump,pv->mk_not(q))),ci);
if(pv->is_sat(s)){
std::cout << "interpolation invariant violated at step " << i << "\n";
assert(0 && "interpolation invariant violated");
}
}
if((*parents)[this_frame] == 39)
child_interps[i] = pv->mk_and(child_interps[i],q);
#endif
}
ast &bar = itps[nodes.size()-1];
#ifdef FACTOR_INTERPS
if(!weak)
bar = my_or(bar,disj_of_set(disjs[nodes.size()-1]));
else
bar = pv->mk_and(bar,pv->mk_not(disj_of_set(disjs[nodes.size()-1])));
#endif
profiling::timer_stop("interp_proof");
profiling::timer_start("simplifying");
bar = pv->simplify(bar);
profiling::timer_stop("simplifying");
return bar;
}
void iz3proof::print(std::ostream &s, int id){
node_struct &n = nodes[id];
switch(n.rl){
case Assumption:
s << "Assumption(";
pv->print_clause(s,n.conclusion);
s << ")";
break;
case Hypothesis:
s << "Hyp("; pv->print_expr(s,n.conclusion[0]); s << ")"; break;
case Reflexivity:
s << "Refl("; pv->print_expr(s,n.conclusion[0]); s << ")"; break;
case Symmetry:
s << "Symm("; print(s,n.premises[0]); s << ")"; break;
case Transitivity:
s << "Trans("; print(s,n.premises[0]); s << ","; print(s,n.premises[1]); s << ")"; break;
case Congruence:
s << "Cong("; pv->print_expr(s,n.conclusion[0]);
for(unsigned i = 0; i < n.premises.size(); i++){
s << ",";
print(s,n.premises[i]);
}
s << ")"; break;
case EqContra:
s << "EqContra("; print(s,n.premises[0]); s << ","; print(s,n.premises[1]); s << ")"; break;
case Resolution:
s << "Res(";
pv->print_expr(s,n.aux); s << ",";
print(s,n.premises[0]); s << ","; print(s,n.premises[1]); s << ")";
break;
case Lemma:
s << "Lemma(";
pv->print_clause(s,n.conclusion);
for(unsigned i = 0; i < n.premises.size(); i++){
s << ",";
print(s,n.premises[i]);
}
s << ")";
break;
case Contra:
s << "Contra(";
print(s,n.premises[0]);
s << ")";
break;
default:;
}
}
void iz3proof::show(int id){
std::ostringstream ss;
print(ss,id);
iz3base::pretty_print(std::cout,ss.str());
// std::cout << ss.str();
std::cout << "\n";
}

274
src/interp/iz3proof.h
View file

@ -1,274 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
iz3proof.h
Abstract:
This class defines a simple interpolating proof system.
Author:
Ken McMillan (kenmcmil)
Revision History:
--*/
#ifndef IZ3PROOF_H
#define IZ3PROOF_H
#include <set>
#include "interp/iz3base.h"
#include "interp/iz3secondary.h"
// #define CHECK_PROOFS
/** This class defines a simple proof system.
A proof is a dag consisting of "nodes". The children of each node
are its "premises". Each node has a "conclusion" that is a clause,
represented as a vector of literals.
The literals are represented by abstract syntax trees. Operations
on these, including computation of scopes are provided by iz3base.
A proof can be interpolated, provided it is restricted to the
rules Resolution, Assumption, Contra and Lemma, and that all
clauses are strict (i.e., each literal in each clause is local).
*/
class iz3proof {
public:
/** The type of proof nodes (nodes in the derivation tree). */
typedef int node;
/** Enumeration of proof rules. */
enum rule {Resolution,Assumption,Hypothesis,Theory,Axiom,Contra,Lemma,Reflexivity,Symmetry,Transitivity,Congruence,EqContra};
/** Interface to prover. */
typedef iz3base prover;
/** Ast type. */
typedef prover::ast ast;
/** Object thrown in case of a proof error. */
struct proof_error: public iz3_exception {
proof_error(): iz3_exception("proof_error") {}
};
/* Null proof node */
static const node null = -1;
/** Make a resolution node with given pivot liter and premises.
The conclusion of premise1 should contain the negation of the
pivot literal, while the conclusion of premise2 should containe the
pivot literal.
*/
node make_resolution(ast pivot, node premise1, node premise2);
/** Make an assumption node. The given clause is assumed in the given frame. */
node make_assumption(int frame, const std::vector<ast> &assumption);
/** Make a hypothesis node. If phi is the hypothesis, this is
effectively phi |- phi. */
node make_hypothesis(ast hypothesis);
/** Make a theory node. This can be any inference valid in the theory. */
node make_theory(const std::vector<ast> &conclusion, std::vector<node> premises);
/** Make an axiom node. The conclusion must be an instance of an axiom. */
node make_axiom(const std::vector<ast> &conclusion);
/** Make a Contra node. This rule takes a derivation of the form
Gamma |- False and produces |- \/~Gamma. */
node make_contra(node prem, const std::vector<ast> &conclusion);
/** Make a lemma node. A lemma node must have an interpolation. */
node make_lemma(const std::vector<ast> &conclusion, const std::vector<ast> &interpolation);
/** Make a Reflexivity node. This rule produces |- x = x */
node make_reflexivity(ast con);
/** Make a Symmetry node. This takes a derivation of |- x = y and
produces | y = x */
node make_symmetry(ast con, node prem);
/** Make a transitivity node. This takes derivations of |- x = y
and |- y = z produces | x = z */
node make_transitivity(ast con, node prem1, node prem2);
/** Make a congruence node. This takes derivations of |- x_i = y_i
and produces |- f(x_1,...,x_n) = f(y_1,...,y_n) */
node make_congruence(ast con, const std::vector<node> &prems);
/** Make an equality contradicition node. This takes |- x = y
and |- !(x = y) and produces false. */
node make_eqcontra(node prem1, node prem2);
/** Get the rule of a node in a proof. */
rule get_rule(node n){
return nodes[n].rl;
}
/** Get the pivot of a resolution node. */
ast get_pivot(node n){
return nodes[n].aux;
}
/** Get the frame of an assumption node. */
int get_frame(node n){
return nodes[n].frame;
}
/** Get the number of literals of the conclusion of a node. */
int get_num_conclusion_lits(node n){
return get_conclusion(n).size();
}
/** Get the nth literal of the conclusion of a node. */
ast get_nth_conclusion_lit(node n, int i){
return get_conclusion(n)[i];
}
/** Get the conclusion of a node. */
void get_conclusion(node n, std::vector<ast> &result){
result = get_conclusion(n);
}
/** Get the number of premises of a node. */
int get_num_premises(node n){
return nodes[n].premises.size();
}
/** Get the nth premise of a node. */
int get_nth_premise(node n, int i){
return nodes[n].premises[i];
}
/** Get all the premises of a node. */
void get_premises(node n, std::vector<node> &result){
result = nodes[n].premises;
}
/** Create a new proof node, replacing the premises of an old
one. */
node clone(node n, std::vector<node> &premises){
if(premises == nodes[n].premises)
return n;
nodes.push_back(nodes[n]);
nodes.back().premises = premises;
return nodes.size()-1;
}
/** Copy a proof node from src */
node copy(iz3proof &src, node n);
/** Resolve two lemmas on a given literal. */
node resolve_lemmas(ast pivot, node left, node right);
/** Swap two proofs. */
void swap(iz3proof &other){
std::swap(pv,other.pv);
nodes.swap(other.nodes);
interps.swap(other.interps);
}
/** Compute an interpolant for a proof, where the "A" side is defined by
the given range of frames. Parameter "weak", when true, uses different
interpolation system that resutls in generally weaker interpolants.
*/
ast interpolate(const prover::range &_rng, bool weak = false
#ifdef CHECK_PROOFS
, Z3_ast assump = (Z3_ast)0, std::vector<int> *parents = 0
#endif
);
/** print proof node to a stream */
void print(std::ostream &s, node n);
/** show proof node on stdout */
void show(node n);
/** Construct a proof, with a given prover. */
iz3proof(prover *p){
pv = p;
}
/** Default constructor */
iz3proof(){pv = nullptr;}
protected:
struct node_struct {
rule rl;
ast aux;
int frame;
std::vector<ast> conclusion;
std::vector<node> premises;
};
std::vector<node_struct> nodes;
std::vector<std::vector<ast> > interps; // interpolations of lemmas
prover *pv;
node make_node(){
nodes.push_back(node_struct());
return nodes.size()-1;
}
void resolve(ast pivot, std::vector<ast> &cls1, const std::vector<ast> &cls2);
node copy_rec(stl_ext::hash_map<node,node> &memo, iz3proof &src, node n);
void interpolate_lemma(node_struct &n);
// lazily compute the result of resolution
// the node member "frame" indicates result is computed
const std::vector<ast> &get_conclusion(node x){
node_struct &n = nodes[x];
if(n.rl == Resolution && !n.frame){
n.conclusion = get_conclusion(n.premises[0]);
resolve(n.aux,n.conclusion,get_conclusion(n.premises[1]));
n.frame = 1;
}
return n.conclusion;
}
prover::range rng;
bool weak;
stl_ext::hash_set<ast> b_lits;
ast my_or(ast x, ast y);
#ifdef CHECK_PROOFS
std::vector<Z3_ast> child_interps;
#endif
bool pred_in_A(ast id);
bool term_in_B(ast id);
bool frame_in_A(int frame);
bool lit_in_B(ast lit);
ast get_A_lits(std::vector<ast> &cls);
ast get_B_lits(std::vector<ast> &cls);
void find_B_lits();
ast disj_of_set(std::set<ast> &s);
void mk_or_factor(int p1, int p2, int i, std::vector<ast> &itps, std::vector<std::set<ast> > &disjs);
void mk_and_factor(int p1, int p2, int i, std::vector<ast> &itps, std::vector<std::set<ast> > &disjs);
void set_of_B_lits(std::vector<ast> &cls, std::set<ast> &res);
void set_of_A_lits(std::vector<ast> &cls, std::set<ast> &res);
};
#endif

3117
src/interp/iz3proof_itp.cpp
View file

File diff suppressed because it is too large Load diff

143
src/interp/iz3proof_itp.h
View file

@ -1,143 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
iz3proof.h
Abstract:
This class defines a simple interpolating proof system.
Author:
Ken McMillan (kenmcmil)
Revision History:
--*/
#ifndef IZ3PROOF_ITP_H
#define IZ3PROOF_ITP_H
#include <set>
#include "interp/iz3base.h"
#include "interp/iz3secondary.h"
// #define CHECK_PROOFS
/** This class defines a simple proof system.
As opposed to iz3proof, this class directly computes interpolants,
so the proof representation is just the interpolant itself.
*/
class iz3proof_itp : public iz3mgr {
public:
/** Enumeration of proof rules. */
enum rule {Resolution,Assumption,Hypothesis,Theory,Axiom,Contra,Lemma,Reflexivity,Symmetry,Transitivity,Congruence,EqContra};
/** Interface to prover. */
typedef iz3base prover;
/** Ast type. */
typedef prover::ast ast;
/** The type of proof nodes (just interpolants). */
typedef ast node;
/** Object thrown in case of a proof error. */
struct proof_error: public iz3_exception {
proof_error(): iz3_exception("proof_error") {}
};
/** Make a resolution node with given pivot literal and premises.
The conclusion of premise1 should contain the negation of the
pivot literal, while the conclusion of premise2 should containe the
pivot literal.
*/
virtual node make_resolution(ast pivot, const std::vector<ast> &conc, node premise1, node premise2) = 0;
/** Make an assumption node. The given clause is assumed in the given frame. */
virtual node make_assumption(int frame, const std::vector<ast> &assumption) = 0;
/** Make a hypothesis node. If phi is the hypothesis, this is
effectively phi |- phi. */
virtual node make_hypothesis(const ast &hypothesis) = 0;
/** Make an axiom node. The conclusion must be an instance of an axiom. */
virtual node make_axiom(const std::vector<ast> &conclusion) = 0;
/** Make an axiom node. The conclusion must be an instance of an axiom. Localize axiom instance to range*/
virtual node make_axiom(const std::vector<ast> &conclusion, prover::range) = 0;
/** Make a Contra node. This rule takes a derivation of the form
Gamma |- False and produces |- \/~Gamma. */
virtual node make_contra(node prem, const std::vector<ast> &conclusion) = 0;
/** Make a Reflexivity node. This rule produces |- x = x */
virtual node make_reflexivity(ast con) = 0;
/** Make a Symmetry node. This takes a derivation of |- x = y and
produces | y = x */
virtual node make_symmetry(ast con, const ast &premcon, node prem) = 0;
/** Make a transitivity node. This takes derivations of |- x = y
and |- y = z produces | x = z */
virtual node make_transitivity(const ast &x, const ast &y, const ast &z, node prem1, node prem2) = 0;
/** Make a congruence node. This takes a derivation of |- x_i = y_i
and produces |- f(...x_i,...) = f(...,y_i,...) */
virtual node make_congruence(const ast &xi_eq_yi, const ast &con, const ast &prem1) = 0;
/** Make a congruence node. This takes derivations of |- x_i1 = y_i1, |- x_i2 = y_i2,...
and produces |- f(...x_i1...x_i2...) = f(...y_i1...y_i2...) */
virtual node make_congruence(const std::vector<ast> &xi_eq_yi, const ast &con, const std::vector<ast> &prems) = 0;
/** Make a modus-ponens node. This takes derivations of |- x
and |- x = y and produces |- y */
virtual node make_mp(const ast &x_eq_y, const ast &prem1, const ast &prem2) = 0;
/** Make a farkas proof node. */
virtual node make_farkas(ast con, const std::vector<node> &prems, const std::vector<ast> &prem_cons, const std::vector<ast> &coeffs) = 0;
/* Make an axiom instance of the form |- x<=y, y<= x -> x =y */
virtual node make_leq2eq(ast x, ast y, const ast &xleqy, const ast &yleqx) = 0;
/* Make an axiom instance of the form |- x = y -> x <= y */
virtual node make_eq2leq(ast x, ast y, const ast &xeqy) = 0;
/* Make an inference of the form t <= c |- t/d <= floor(c/d) where t
is an affine term divisble by d and c is an integer constant */
virtual node make_cut_rule(const ast &tleqc, const ast &d, const ast &con, const ast &prem) = 0;
/* Return an interpolant from a proof of false */
virtual ast interpolate(const node &pf) = 0;
/** Create proof object to construct an interpolant. */
static iz3proof_itp *create(prover *p, const prover::range &r, bool _weak);
protected:
iz3proof_itp(iz3mgr &m)
: iz3mgr(m)
{
}
public:
virtual ~iz3proof_itp(){
}
};
#endif

321
src/interp/iz3scopes.cpp
View file

@ -1,321 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
iz3scopes.cpp
Abstract:
Calculations with scopes, for both sequence and tree interpolation.
Author:
Ken McMillan (kenmcmil)
Revision History:
--*/
#include <assert.h>
#include <algorithm>
#include "interp/iz3scopes.h"
/** computes the least common ancestor of two nodes in the tree, or SHRT_MAX if none */
int scopes::tree_lca(int n1, int n2){
if(!tree_mode())
return std::max(n1,n2);
if(n1 == SHRT_MIN) return n2;
if(n2 == SHRT_MIN) return n1;
if(n1 == SHRT_MAX || n2 == SHRT_MAX) return SHRT_MAX;
while(n1 != n2){
if(n1 == SHRT_MAX || n2 == SHRT_MAX) return SHRT_MAX;
assert(n1 >= 0 && n2 >= 0 && n1 < (int)parents.size() && n2 < (int)parents.size());
if(n1 < n2) n1 = parents[n1];
else n2 = parents[n2];
}
return n1;
}
/** computes the greatest common descendant two nodes in the tree, or SHRT_MIN if none */
int scopes::tree_gcd(int n1, int n2){
if(!tree_mode())
return std::min(n1,n2);
int foo = tree_lca(n1,n2);
if(foo == n1) return n2;
if(foo == n2) return n1;
return SHRT_MIN;
}
#ifndef FULL_TREE
/** test whether a tree node is contained in a range */
bool scopes::in_range(int n, const range &rng){
return tree_lca(rng.lo,n) == n && tree_gcd(rng.hi,n) == n;
}
/** test whether two ranges of tree nodes intersect */
bool scopes::ranges_intersect(const range &rng1, const range &rng2){
return tree_lca(rng1.lo,rng2.hi) == rng2.hi && tree_lca(rng1.hi,rng2.lo) == rng1.hi;
}
bool scopes::range_contained(const range &rng1, const range &rng2){
return tree_lca(rng2.lo,rng1.lo) == rng1.lo
&& tree_lca(rng1.hi,rng2.hi) == rng2.hi;
}
scopes::range scopes::range_lub(const range &rng1, const range &rng2){
range res;
res.lo = tree_gcd(rng1.lo,rng2.lo);
res.hi = tree_lca(rng1.hi,rng2.hi);
return res;
}
scopes::range scopes::range_glb(const range &rng1, const range &rng2){
range res;
res.lo = tree_lca(rng1.lo,rng2.lo);
res.hi = tree_gcd(rng1.hi,rng2.hi);
return res;
}
#else
namespace std {
template <>
class hash<scopes::range_lo > {
public:
size_t operator()(const scopes::range_lo &p) const {
return p.lo + (size_t)p.next;
}
};
}
template <> inline
size_t stdext::hash_value<scopes::range_lo >(const scopes::range_lo& p)
{
std::hash<scopes::range_lo> h;
return h(p);
}
namespace std {
template <>
class less<scopes::range_lo > {
public:
bool operator()(const scopes::range_lo &x, const scopes::range_lo &y) const {
return x.lo < y.lo || x.lo == y.lo && (size_t)x.next < (size_t)y.next;
}
};
}
struct range_op {
scopes::range_lo *x, *y;
int hi;
range_op(scopes::range_lo *_x, scopes::range_lo *_y, int _hi){
x = _x; y = _y; hi = _hi;
}
};
namespace std {
template <>
class hash<range_op > {
public:
size_t operator()(const range_op &p) const {
return (size_t) p.x + (size_t)p.y + p.hi;
}
};
}
template <> inline
size_t stdext::hash_value<range_op >(const range_op& p)
{
std::hash<range_op> h;
return h(p);
}
namespace std {
template <>
class less<range_op > {
public:
bool operator()(const range_op &x, const range_op &y) const {
return (size_t)x.x < (size_t)y.x || x.x == y.x &&
((size_t)x.y < (size_t)y.y || x.y == y.y && x.hi < y.hi);
}
};
}
struct range_tables {
hash_map<scopes::range_lo, scopes::range_lo *> unique;
hash_map<range_op,scopes::range_lo *> lub;
hash_map<range_op,scopes::range_lo *> glb;
};
scopes::range_lo *scopes::find_range_lo(int lo, range_lo *next){
range_lo foo(lo,next);
std::pair<range_lo,range_lo *> baz(foo,(range_lo *)0);
std::pair<hash_map<range_lo,scopes::range_lo *>::iterator,bool> bar = rt->unique.insert(baz);
if(bar.second)
bar.first->second = new range_lo(lo,next);
return bar.first->second;
//std::pair<hash_set<scopes::range_lo>::iterator,bool> bar = rt->unique.insert(foo);
// const range_lo *baz = &*(bar.first);
// return (range_lo *)baz; // coerce const
}
scopes::range_lo *scopes::range_lub_lo(range_lo *rng1, range_lo *rng2){
if(!rng1) return rng2;
if(!rng2) return rng1;
if(rng1->lo > rng2->lo)
std::swap(rng1,rng2);
std::pair<range_op,range_lo *> foo(range_op(rng1,rng2,0),(range_lo *)0);
std::pair<hash_map<range_op,scopes::range_lo *>::iterator,bool> bar = rt->lub.insert(foo);
range_lo *&res = bar.first->second;
if(!bar.second) return res;
if(!(rng1->next && rng1->next->lo <= rng2->lo)){
for(int lo = rng1->lo; lo <= rng2->lo; lo = parents[lo])
if(lo == rng2->lo)
{rng2 = rng2->next; break;}
}
range_lo *baz = range_lub_lo(rng1->next,rng2);
res = find_range_lo(rng1->lo,baz);
return res;
}
scopes::range_lo *scopes::range_glb_lo(range_lo *rng1, range_lo *rng2, int hi){
if(!rng1) return rng1;
if(!rng2) return rng2;
if(rng1->lo > rng2->lo)
std::swap(rng1,rng2);
std::pair<range_op,range_lo *> cand(range_op(rng1,rng2,hi),(range_lo *)0);
std::pair<hash_map<range_op,scopes::range_lo *>::iterator,bool> bar = rt->glb.insert(cand);
range_lo *&res = bar.first->second;
if(!bar.second) return res;
range_lo *foo;
if(!(rng1->next && rng1->next->lo <= rng2->lo)){
int lim = hi;
if(rng1->next) lim = std::min(lim,rng1->next->lo);
int a = rng1->lo, b = rng2->lo;
while(a != b && b <= lim){
a = parents[a];
if(a > b)std::swap(a,b);
}
if(a == b && b <= lim){
foo = range_glb_lo(rng1->next,rng2->next,hi);
foo = find_range_lo(b,foo);
}
else
foo = range_glb_lo(rng2,rng1->next,hi);
}
else foo = range_glb_lo(rng1->next,rng2,hi);
res = foo;
return res;
}
/** computes the lub (smallest containing subtree) of two ranges */
scopes::range scopes::range_lub(const range &rng1, const range &rng2){
int hi = tree_lca(rng1.hi,rng2.hi);
if(hi == SHRT_MAX) return range_full();
range_lo *lo = range_lub_lo(rng1.lo,rng2.lo);
return range(hi,lo);
}
/** computes the glb (intersection) of two ranges */
scopes::range scopes::range_glb(const range &rng1, const range &rng2){
if(rng1.hi == SHRT_MAX) return rng2;
if(rng2.hi == SHRT_MAX) return rng1;
int hi = tree_gcd(rng1.hi,rng2.hi);
range_lo *lo = hi == SHRT_MIN ? 0 : range_glb_lo(rng1.lo,rng2.lo,hi);
if(!lo) hi = SHRT_MIN;
return range(hi,lo);
}
/** is this range empty? */
bool scopes::range_is_empty(const range &rng){
return rng.hi == SHRT_MIN;
}
/** return an empty range */
scopes::range scopes::range_empty(){
return range(SHRT_MIN,0);
}
/** return a full range */
scopes::range scopes::range_full(){
return range(SHRT_MAX,0);
}
/** return the maximal element of a range */
int scopes::range_max(const range &rng){
return rng.hi;
}
/** return a minimal (not necessarily unique) element of a range */
int scopes::range_min(const range &rng){
if(rng.hi == SHRT_MAX) return SHRT_MIN;
return rng.lo ? rng.lo->lo : SHRT_MAX;
}
/** return range consisting of downward closure of a point */
scopes::range scopes::range_downward(int _hi){
std::vector<bool> descendants(parents.size());
for(int i = descendants.size() - 1; i >= 0 ; i--)
descendants[i] = i == _hi || parents[i] < parents.size() && descendants[parents[i]];
for(unsigned i = 0; i < descendants.size() - 1; i++)
if(parents[i] < parents.size())
descendants[parents[i]] = false;
range_lo *foo = 0;
for(int i = descendants.size() - 1; i >= 0; --i)
if(descendants[i]) foo = find_range_lo(i,foo);
return range(_hi,foo);
}
/** add an element to a range */
void scopes::range_add(int i, range &n){
range foo = range(i, find_range_lo(i,0));
n = range_lub(foo,n);
}
/** Choose an element of rng1 that is near to rng2 */
int scopes::range_near(const range &rng1, const range &rng2){
int frame;
int thing = tree_lca(rng1.hi,rng2.hi);
if(thing != rng1.hi) return rng1.hi;
range line = range(rng1.hi,find_range_lo(rng2.hi,(range_lo *)0));
line = range_glb(line,rng1);
return range_min(line);
}
/** test whether a tree node is contained in a range */
bool scopes::in_range(int n, const range &rng){
range r = range_empty();
range_add(n,r);
r = range_glb(rng,r);
return !range_is_empty(r);
}
/** test whether two ranges of tree nodes intersect */
bool scopes::ranges_intersect(const range &rng1, const range &rng2){
range r = range_glb(rng1,rng2);
return !range_is_empty(r);
}
bool scopes::range_contained(const range &rng1, const range &rng2){
range r = range_glb(rng1,rng2);
return r.hi == rng1.hi && r.lo == rng1.lo;
}
#endif

222
src/interp/iz3scopes.h
View file

@ -1,222 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
iz3scopes.h
Abstract:
Calculations with scopes, for both sequence and tree interpolation.
Author:
Ken McMillan (kenmcmil)
Revision History:
--*/
#ifndef IZ3SOPES_H
#define IZ3SOPES_H
#include <vector>
#include <limits.h>
#include "interp/iz3hash.h"
class scopes {
public:
/** Construct from parents vector. */
scopes(const std::vector<int> &_parents){
parents = _parents;
}
scopes(){
}
void initialize(const std::vector<int> &_parents){
parents = _parents;
}
/** The parents vector defining the tree structure */
std::vector<int> parents;
// #define FULL_TREE
#ifndef FULL_TREE
struct range {
range(){
lo = SHRT_MAX;
hi = SHRT_MIN;
}
short lo, hi;
};
/** computes the lub (smallest containing subtree) of two ranges */
range range_lub(const range &rng1, const range &rng2);
/** computes the glb (intersection) of two ranges */
range range_glb(const range &rng1, const range &rng2);
/** is this range empty? */
bool range_is_empty(const range &rng){
return rng.hi < rng.lo;
}
/** is this range full? */
bool range_is_full(const range &rng){
return rng.lo == SHRT_MIN && rng.hi == SHRT_MAX;
}
/** return an empty range */
range range_empty(){
range res;
res.lo = SHRT_MAX;
res.hi = SHRT_MIN;
return res;
}
/** return an empty range */
range range_full(){
range res;
res.lo = SHRT_MIN;
res.hi = SHRT_MAX;
return res;
}
/** return the maximal element of a range */
int range_max(const range &rng){
return rng.hi;
}
/** return a minimal (not necessarily unique) element of a range */
int range_min(const range &rng){
return rng.lo;
}
/** return range consisting of downward closure of a point */
range range_downward(int _hi){
range foo;
foo.lo = SHRT_MIN;
foo.hi = _hi;
return foo;
}
void range_add(int i, range &n){
#if 0
if(i < n.lo) n.lo = i;
if(i > n.hi) n.hi = i;
#else
range rng; rng.lo = i; rng.hi = i;
n = range_lub(rng,n);
#endif
}
/** Choose an element of rng1 that is near to rng2 */
int range_near(const range &rng1, const range &rng2){
int frame;
int thing = tree_lca(rng1.lo,rng2.hi);
if(thing == rng1.lo) frame = rng1.lo;
else frame = tree_gcd(thing,rng1.hi);
return frame;
}
#else
struct range_lo {
int lo;
range_lo *next;
range_lo(int _lo, range_lo *_next){
lo = _lo;
next = _next;
}
};
struct range {
int hi;
range_lo *lo;
range(int _hi, range_lo *_lo){
hi = _hi;
lo = _lo;
}
range(){
hi = SHRT_MIN;
lo = 0;
}
};
range_tables *rt;
/** computes the lub (smallest containing subtree) of two ranges */
range range_lub(const range &rng1, const range &rng2);
/** computes the glb (intersection) of two ranges */
range range_glb(const range &rng1, const range &rng2);
/** is this range empty? */
bool range_is_empty(const range &rng);
/** return an empty range */
range range_empty();
/** return a full range */
range range_full();
/** return the maximal element of a range */
int range_max(const range &rng);
/** return a minimal (not necessarily unique) element of a range */
int range_min(const range &rng);
/** return range consisting of downward closure of a point */
range range_downward(int _hi);
/** add an element to a range */
void range_add(int i, range &n);
/** Choose an element of rng1 that is near to rng2 */
int range_near(const range &rng1, const range &rng2);
range_lo *find_range_lo(int lo, range_lo *next);
range_lo *range_lub_lo(range_lo *rng1, range_lo *rng2);
range_lo *range_glb_lo(range_lo *rng1, range_lo *rng2, int lim);
#endif
/** test whether a tree node is contained in a range */
bool in_range(int n, const range &rng);
/** test whether two ranges of tree nodes intersect */
bool ranges_intersect(const range &rng1, const range &rng2);
/** test whether range rng1 contained in range rng2 */
bool range_contained(const range &rng1, const range &rng2);
private:
int tree_lca(int n1, int n2);
int tree_gcd(int n1, int n2);
bool tree_mode(){return parents.size() != 0;}
};
// let us hash on ranges
#ifndef FULL_TREE
namespace hash_space {
template <>
class hash<scopes::range> {
public:
size_t operator()(const scopes::range &p) const {
return (size_t)p.lo + (size_t)p.hi;
}
};
}
inline bool operator==(const scopes::range &x, const scopes::range &y){
return x.lo == y.lo && x.hi == y.hi;
}
#endif
#endif

40
src/interp/iz3secondary.h
View file

@ -1,40 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
iz3secondary
Abstract:
Interface for secondary provers.
Author:
Ken McMillan (kenmcmil)
Revision History:
--*/
#ifndef IZ3SECONDARY_H
#define IZ3SECONDARY_H
/** Interface class for secondary provers. */
#include "interp/iz3base.h"
#include <vector>
class iz3secondary : public iz3mgr {
public:
virtual int interpolate(const std::vector<ast> &frames, std::vector<ast> &interpolants) = 0;
virtual ~iz3secondary(){}
protected:
iz3secondary(const iz3mgr &mgr) : iz3mgr(mgr) {}
};
#endif

2200
src/interp/iz3translate.cpp
View file

File diff suppressed because it is too large Load diff

63
src/interp/iz3translate.h
View file

@ -1,63 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
iz3translate.h
Abstract:
Interface for proof translations from Z3 proofs to interpolatable
proofs.
Author:
Ken McMillan (kenmcmil)
Revision History:
--*/
#ifndef IZ3TRANSLATION_H
#define IZ3TRANSLATION_H
#include "interp/iz3proof.h"
#include "interp/iz3secondary.h"
// This is a interface class for translation from Z3 proof terms to
// an interpolatable proof
class iz3translation : public iz3base {
public:
virtual iz3proof::node translate(ast, iz3proof &) = 0;
virtual ast quantify(ast e, const range &rng){return e;}
virtual ~iz3translation(){}
/** This is thrown when the proof cannot be translated. */
struct unsupported: public iz3_exception {
raw_ast* m_ast;
unsupported(ast const& a): iz3_exception("unsupported"), m_ast(a.raw()) { }
};
static iz3translation *create(iz3mgr &mgr,
iz3secondary *secondary,
const std::vector<std::vector<ast> > &frames,
const std::vector<int> &parents,
const std::vector<ast> &theory);
protected:
iz3translation(iz3mgr &mgr,
const std::vector<std::vector<ast> > &_cnsts,
const std::vector<int> &_parents,
const std::vector<ast> &_theory)
: iz3base(mgr,_cnsts,_parents,_theory) {}
};
// To use a secondary prover, define IZ3_TRANSLATE_DIRECT instead of this
#define IZ3_TRANSLATE_FULL
#endif

1717
src/interp/iz3translate_direct.cpp
View file

File diff suppressed because it is too large Load diff

15
src/muz/base/dl_context.cpp
View file

@ -188,7 +188,7 @@ namespace datalog {
if (m_trail.get_num_scopes() == 0) {
throw default_exception("there are no backtracking points to pop to");
}
if (m_engine.get() && get_engine() != DUALITY_ENGINE) {
if (m_engine.get()) {
throw default_exception("pop operation is only supported by duality engine");
}
m_trail.pop_scope(1);
@ -601,11 +601,6 @@ namespace datalog {
m_rule_properties.check_existential_tail();
m_rule_properties.check_for_negated_predicates();
break;
case DUALITY_ENGINE:
m_rule_properties.collect(r);
m_rule_properties.check_existential_tail();
m_rule_properties.check_for_negated_predicates();
break;
case CLP_ENGINE:
m_rule_properties.collect(r);
m_rule_properties.check_existential_tail();
@ -828,9 +823,6 @@ namespace datalog {
else if (e == symbol("clp")) {
m_engine_type = CLP_ENGINE;
}
else if (e == symbol("duality")) {
m_engine_type = DUALITY_ENGINE;
}
else if (e == symbol("ddnf")) {
m_engine_type = DDNF_ENGINE;
}
@ -875,11 +867,6 @@ namespace datalog {
case DDNF_ENGINE:
flush_add_rules();
break;
case DUALITY_ENGINE:
// this lets us use duality with SAS 2013 abstraction
if(quantify_arrays())
flush_add_rules();
break;
default:
UNREACHABLE();
}

1
src/muz/base/dl_engine_base.h
View file

@ -32,7 +32,6 @@ namespace datalog {
QBMC_ENGINE,
TAB_ENGINE,
CLP_ENGINE,
DUALITY_ENGINE,
DDNF_ENGINE,
LAST_ENGINE
};

8
src/muz/duality/CMakeLists.txt
View file

@ -1,8 +0,0 @@
z3_add_component(duality_intf
SOURCES
duality_dl_interface.cpp
COMPONENT_DEPENDENCIES
duality
muz
transforms
)

623
src/muz/duality/duality_dl_interface.cpp
View file

@ -1,623 +0,0 @@
/*++
Copyright (c) 2013 Microsoft Corporation
Module Name:
duality_dl_interface.cpp
Abstract:
SMT2 interface for Duality
Author:
Krystof Hoder (t-khoder) 2011-9-22.
Modified by Ken McMIllan (kenmcmil) 2013-4-18.
Revision History:
--*/
#include "muz/base/dl_context.h"
#include "muz/transforms/dl_mk_coi_filter.h"
#include "muz/transforms/dl_mk_interp_tail_simplifier.h"
#include "muz/transforms/dl_mk_subsumption_checker.h"
#include "muz/transforms/dl_mk_rule_inliner.h"
#include "muz/base/dl_rule.h"
#include "muz/base/dl_rule_transformer.h"
#include "parsers/smt2/smt2parser.h"
#include "muz/duality/duality_dl_interface.h"
#include "muz/base/dl_rule_set.h"
#include "muz/transforms/dl_mk_slice.h"
#include "muz/transforms/dl_mk_unfold.h"
#include "muz/transforms/dl_mk_coalesce.h"
#include "ast/expr_abstract.h"
#include "model/model_smt2_pp.h"
#include "model/model_v2_pp.h"
#include "muz/base/fixedpoint_params.hpp"
#include "ast/used_vars.h"
#include "ast/func_decl_dependencies.h"
#include "muz/transforms/dl_transforms.h"
// template class symbol_table<family_id>;
#ifdef WIN32
#pragma warning(disable:4996)
#pragma warning(disable:4800)
#pragma warning(disable:4267)
#pragma warning(disable:4101)
#endif
#include "duality/duality.h"
#include "duality/duality_profiling.h"
// using namespace Duality;
namespace Duality {
enum DualityStatus {StatusModel, StatusRefutation, StatusUnknown, StatusNull};
class duality_data {
public:
context ctx;
RPFP::LogicSolver *ls;
RPFP *rpfp;
DualityStatus status;
std::vector<expr> clauses;
std::vector<std::vector<RPFP::label_struct> > clause_labels;
hash_map<RPFP::Edge *,int> map; // edges to clauses
Solver *old_rs;
Solver::Counterexample cex;
duality_data(ast_manager &_m) : ctx(_m,config(params_ref())) {
ls = nullptr;
rpfp = nullptr;
status = StatusNull;
old_rs = nullptr;
}
~duality_data(){
if(old_rs)
dealloc(old_rs);
if(rpfp)
dealloc(rpfp);
if(ls)
dealloc(ls);
}
};
dl_interface::dl_interface(datalog::context& dl_ctx) :
engine_base(dl_ctx.get_manager(), "duality"),
m_ctx(dl_ctx)
{
_d = nullptr;
// dl_ctx.get_manager().toggle_proof_mode(PGM_FINE);
}
dl_interface::~dl_interface() {
if(_d)
dealloc(_d);
}
//
// Check if the new rules are weaker so that we can
// re-use existing context.
//
#if 0
void dl_interface::check_reset() {
// TODO
datalog::rule_ref_vector const& new_rules = m_ctx.get_rules().get_rules();
datalog::rule_ref_vector const& old_rules = m_old_rules.get_rules();
bool is_subsumed = !old_rules.empty();
for (unsigned i = 0; is_subsumed && i < new_rules.size(); ++i) {
is_subsumed = false;
for (unsigned j = 0; !is_subsumed && j < old_rules.size(); ++j) {
if (m_ctx.check_subsumes(*old_rules[j], *new_rules[i])) {
is_subsumed = true;
}
}
if (!is_subsumed) {
TRACE("pdr", new_rules[i]->display(m_ctx, tout << "Fresh rule "););
m_context->reset();
}
}
m_old_rules.reset();
m_old_rules.add_rules(new_rules.size(), new_rules.c_ptr());
}
#endif
lbool dl_interface::query(::expr * query) {
// we restore the initial state in the datalog context
m_ctx.ensure_opened();
// if there is old data, get the cex and dispose (later)
duality_data *old_data = _d;
Solver *old_rs = nullptr;
if(old_data){
old_rs = old_data->old_rs;
old_rs->GetCounterexample().swap(old_data->cex);
}
scoped_proof generate_proofs_please(m_ctx.get_manager());
// make a new problem and solver
_d = alloc(duality_data,m_ctx.get_manager());
_d->ctx.set("mbqi",m_ctx.get_params().duality_mbqi());
_d->ls = alloc(RPFP::iZ3LogicSolver,_d->ctx);
_d->rpfp = alloc(RPFP,_d->ls);
expr_ref_vector rules(m_ctx.get_manager());
svector< ::symbol> names;
unsigned_vector bounds;
// m_ctx.get_rules_as_formulas(rules, names);
// If using SAS 2013 abstractiion, we need to perform some transforms
expr_ref query_ref(m_ctx.get_manager());
if(m_ctx.quantify_arrays()){
datalog::rule_manager& rm = m_ctx.get_rule_manager();
rm.mk_query(query, m_ctx.get_rules());
apply_default_transformation(m_ctx);
datalog::rule_set &rs = m_ctx.get_rules();
if(m_ctx.get_rules().get_output_predicates().empty())
query_ref = m_ctx.get_manager().mk_false();
else {
func_decl_ref query_pred(m_ctx.get_manager());
query_pred = m_ctx.get_rules().get_output_predicate();
ptr_vector<sort> sorts;
unsigned nargs = query_pred.get()->get_arity();
expr_ref_vector vars(m_ctx.get_manager());
for(unsigned i = 0; i < nargs; i++){
::sort *s = query_pred.get()->get_domain(i);
vars.push_back(m_ctx.get_manager().mk_var(nargs-1-i,s));
}
query_ref = m_ctx.get_manager().mk_app(query_pred.get(),nargs,vars.c_ptr());
query = query_ref.get();
}
unsigned nrules = rs.get_num_rules();
for(unsigned i = 0; i < nrules; i++){
expr_ref f(m_ctx.get_manager());
rm.to_formula(*rs.get_rule(i), f);
rules.push_back(f);
}
}
else
m_ctx.get_raw_rule_formulas(rules, names, bounds);
// get all the rules as clauses
std::vector<expr> &clauses = _d->clauses;
clauses.clear();
for (unsigned i = 0; i < rules.size(); ++i) {
expr e(_d->ctx,rules[i].get());
clauses.push_back(e);
}
std::vector<sort> b_sorts;
std::vector<symbol> b_names;
used_vars uv;
uv.process(query);
unsigned nuv = uv.get_max_found_var_idx_plus_1();
for(int i = nuv-1; i >= 0; i--){ // var indices are backward
::sort * s = uv.get(i);
if(!s)
s = _d->ctx.m().mk_bool_sort(); // missing var, whatever
b_sorts.push_back(sort(_d->ctx,s));
b_names.push_back(symbol(_d->ctx,::symbol(i))); // names?
}
#if 0
// turn the query into a clause
expr q(_d->ctx,m_ctx.bind_variables(query,false));
std::vector<sort> b_sorts;
std::vector<symbol> b_names;
if (q.is_quantifier() && !q.is_quantifier_forall()) {
int bound = q.get_quantifier_num_bound();
for(int j = 0; j < bound; j++){
b_sorts.push_back(q.get_quantifier_bound_sort(j));
b_names.push_back(q.get_quantifier_bound_name(j));
}
q = q.arg(0);
}
#else
expr q(_d->ctx,query);
#endif
expr qc = implies(q,_d->ctx.bool_val(false));
qc = _d->ctx.make_quant(Forall,b_sorts,b_names,qc);
clauses.push_back(qc);
bounds.push_back(UINT_MAX);
// get the background axioms
unsigned num_asserts = m_ctx.get_num_assertions();
for (unsigned i = 0; i < num_asserts; ++i) {
expr e(_d->ctx,m_ctx.get_assertion(i));
_d->rpfp->AssertAxiom(e);
}
// make sure each predicate is the head of at least one clause
func_decl_set heads;
for(unsigned i = 0; i < clauses.size(); i++){
expr cl = clauses[i];
while(true){
if(cl.is_app()){
decl_kind k = cl.decl().get_decl_kind();
if(k == Implies)
cl = cl.arg(1);
else {
heads.insert(cl.decl());
break;
}
}
else if(cl.is_quantifier())
cl = cl.body();
else break;
}
}
ast_ref_vector const &pinned = m_ctx.get_pinned();
for(unsigned i = 0; i < pinned.size(); i++){
::ast *fa = pinned[i];
if(is_func_decl(fa)){
::func_decl *fd = to_func_decl(fa);
if (m_ctx.is_predicate(fd)) {
func_decl f(_d->ctx, fd);
if (!heads.contains(fd)) {
int arity = f.arity();
std::vector<expr> args;
args.reserve(arity);
for (int j = 0; j < arity; j++)
args.push_back(_d->ctx.fresh_func_decl("X", f.domain(j))());
expr c = implies(_d->ctx.bool_val(false), f(args));
c = _d->ctx.make_quant(Forall, args, c);
clauses.push_back(c);
bounds.push_back(UINT_MAX);
}
}
}
}
unsigned rb = m_ctx.get_params().duality_recursion_bound();
std::vector<unsigned> std_bounds;
for(unsigned i = 0; i < bounds.size(); i++){
unsigned b = bounds[i];
if (b == UINT_MAX) b = rb;
std_bounds.push_back(b);
}
// creates 1-1 map between clauses and rpfp edges
_d->rpfp->FromClauses(clauses,&std_bounds);
// populate the edge-to-clause map
for(unsigned i = 0; i < _d->rpfp->edges.size(); ++i)
_d->map[_d->rpfp->edges[i]] = i;
// create a solver object
Solver *rs = Solver::Create("duality", _d->rpfp);
if(old_rs)
rs->LearnFrom(old_rs); // new solver gets hints from old solver
// set its options
IF_VERBOSE(1, rs->SetOption("report","1"););
rs->SetOption("full_expand",m_ctx.get_params().duality_full_expand() ? "1" : "0");
rs->SetOption("no_conj",m_ctx.get_params().duality_no_conj() ? "1" : "0");
rs->SetOption("feasible_edges",m_ctx.get_params().duality_feasible_edges() ? "1" : "0");
rs->SetOption("use_underapprox",m_ctx.get_params().duality_use_underapprox() ? "1" : "0");
rs->SetOption("stratified_inlining",m_ctx.get_params().duality_stratified_inlining() ? "1" : "0");
rs->SetOption("batch_expand",m_ctx.get_params().duality_batch_expand() ? "1" : "0");
rs->SetOption("conjecture_file",m_ctx.get_params().duality_conjecture_file());
rs->SetOption("enable_restarts",m_ctx.get_params().duality_enable_restarts() ? "1" : "0");
#if 0
if(rb != UINT_MAX){
std::ostringstream os; os << rb;
rs->SetOption("recursion_bound", os.str());
}
#endif
// Solve!
bool ans;
try {
ans = rs->Solve();
}
catch (Duality::solver::cancel_exception &exn){
throw default_exception(Z3_CANCELED_MSG);
}
catch (Duality::Solver::Incompleteness &exn){
throw default_exception("incompleteness");
}
// profile!
if(m_ctx.get_params().duality_profile())
print_profile(std::cout);
// save the result and counterexample if there is one
_d->status = ans ? StatusModel : StatusRefutation;
_d->cex.swap(rs->GetCounterexample()); // take ownership of cex
_d->old_rs = rs; // save this for later hints
if(old_data){
dealloc(old_data); // this deallocates the old solver if there is one
}
// dealloc(rs); this is now owned by data
// true means the RPFP problem is SAT, so the query is UNSAT
// but we return undef if the UNSAT result is bounded
if(ans){
if(rs->IsResultRecursionBounded()){
#if 0
m_ctx.set_status(datalog::BOUNDED);
return l_undef;
#else
return l_false;
#endif
}
return l_false;
}
return l_true;
}
expr_ref dl_interface::get_cover_delta(int level, ::func_decl* pred_orig) {
SASSERT(false);
return expr_ref(m_ctx.get_manager());
}
void dl_interface::add_cover(int level, ::func_decl* pred, ::expr* property) {
SASSERT(false);
}
unsigned dl_interface::get_num_levels(::func_decl* pred) {
SASSERT(false);
return 0;
}
void dl_interface::collect_statistics(::statistics& st) const {
}
void dl_interface::reset_statistics() {
}
static hash_set<func_decl> *local_func_decls;
static void print_proof(dl_interface *d, std::ostream& out, RPFP *tree, RPFP::Node *root) {
context &ctx = d->dd()->ctx;
RPFP::Node &node = *root;
RPFP::Edge &edge = *node.Outgoing;
// first, prove the children (that are actually used)
for(unsigned i = 0; i < edge.Children.size(); i++){
if(!tree->Empty(edge.Children[i])){
print_proof(d,out,tree,edge.Children[i]);
}
}
// print the label and the proved fact
out << "(step s!" << node.number;
out << " (" << node.Name.name();
for(unsigned i = 0; i < edge.F.IndParams.size(); i++)
out << " " << tree->Eval(&edge,edge.F.IndParams[i]);
out << ")\n";
// print the rule number
out << " rule!" << node.Outgoing->map->number;
// print the substitution
out << " (subst\n";
RPFP::Edge *orig_edge = edge.map;
int orig_clause = d->dd()->map[orig_edge];
expr &t = d->dd()->clauses[orig_clause];
if (t.is_quantifier() && t.is_quantifier_forall()) {
int bound = t.get_quantifier_num_bound();
std::vector<sort> sorts;
std::vector<symbol> names;
hash_map<int,expr> subst;
for(int j = 0; j < bound; j++){
sort the_sort = t.get_quantifier_bound_sort(j);
symbol name = t.get_quantifier_bound_name(j);
expr skolem = ctx.constant(symbol(ctx,name),sort(ctx,the_sort));
out << " (= " << skolem << " " << tree->Eval(&edge,skolem) << ")\n";
expr local_skolem = tree->Localize(&edge,skolem);
(*local_func_decls).insert(local_skolem.decl());
}
}
out << " )\n";
out << " (labels";
std::vector<symbol> labels;
tree->GetLabels(&edge,labels);
for(unsigned j = 0; j < labels.size(); j++){
out << " " << labels[j];
}
out << " )\n";
// reference the proofs of all the children, in syntactic order
// "true" means the child is not needed
out << " (ref ";
for(unsigned i = 0; i < edge.Children.size(); i++){
if(!tree->Empty(edge.Children[i]))
out << " s!" << edge.Children[i]->number;
else
out << " true";
}
out << " )";
out << ")\n";
}
void dl_interface::display_certificate(std::ostream& out) const {
((dl_interface *)this)->display_certificate_non_const(out);
}
void dl_interface::display_certificate_non_const(std::ostream& out) {
if(_d->status == StatusModel){
ast_manager &m = m_ctx.get_manager();
model_ref md = get_model();
out << "(fixedpoint \n";
model_smt2_pp(out, m, *md.get(), 0);
out << ")\n";
}
else if(_d->status == StatusRefutation){
out << "(derivation\n";
// negation of the query is the last clause -- prove it
hash_set<func_decl> locals;
local_func_decls = &locals;
print_proof(this,out,_d->cex.get_tree(),_d->cex.get_root());
out << ")\n";
out << "(model \n\"";
::model mod(m_ctx.get_manager());
model orig_model = _d->cex.get_tree()->dualModel;
for(unsigned i = 0; i < orig_model.num_consts(); i++){
func_decl cnst = orig_model.get_const_decl(i);
if (locals.find(cnst) == locals.end()) {
expr thing = orig_model.get_const_interp(cnst);
mod.register_decl(to_func_decl(cnst.raw()), to_expr(thing.raw()));
}
}
for(unsigned i = 0; i < orig_model.num_funcs(); i++){
func_decl cnst = orig_model.get_func_decl(i);
if (locals.find(cnst) == locals.end()) {
func_interp thing = orig_model.get_func_interp(cnst);
::func_interp *thing_raw = thing;
mod.register_decl(to_func_decl(cnst.raw()), thing_raw->copy());
}
}
model_v2_pp(out,mod);
out << "\")\n";
}
}
expr_ref dl_interface::get_answer() {
SASSERT(false);
return expr_ref(m_ctx.get_manager());
}
void dl_interface::cancel() {
#if 0
if(_d && _d->ls)
_d->ls->cancel();
#else
// HACK: duality can't cancel at all times, we just exit here
std::cout << "(error \"duality canceled\")\nunknown\n";
abort();
#endif
}
void dl_interface::cleanup() {
}
void dl_interface::updt_params() {
}
model_ref dl_interface::get_model() {
ast_manager &m = m_ctx.get_manager();
model_ref md(alloc(::model, m));
std::vector<RPFP::Node *> &nodes = _d->rpfp->nodes;
expr_ref_vector conjs(m);
for (unsigned i = 0; i < nodes.size(); ++i) {
RPFP::Node *node = nodes[i];
func_decl &pred = node->Name;
expr_ref prop(m);
prop = to_expr(node->Annotation.Formula);
std::vector<expr> &params = node->Annotation.IndParams;
expr_ref q(m);
expr_ref_vector sig_vars(m);
for (unsigned j = 0; j < params.size(); ++j)
sig_vars.push_back(params[params.size()-j-1]); // TODO: why backwards?
expr_abstract(m, 0, sig_vars.size(), sig_vars.c_ptr(), prop, q);
if (params.empty()) {
md->register_decl(pred, q);
}
else {
::func_interp* fi = alloc(::func_interp, m, params.size());
fi->set_else(q);
md->register_decl(pred, fi);
}
}
return md;
}
static proof_ref extract_proof(dl_interface *d, RPFP *tree, RPFP::Node *root) {
context &ctx = d->dd()->ctx;
ast_manager &mgr = ctx.m();
RPFP::Node &node = *root;
RPFP::Edge &edge = *node.Outgoing;
RPFP::Edge *orig_edge = edge.map;
// first, prove the children (that are actually used)
proof_ref_vector prems(mgr);
::vector<expr_ref_vector> substs;
int orig_clause = d->dd()->map[orig_edge];
expr &t = d->dd()->clauses[orig_clause];
prems.push_back(mgr.mk_asserted(ctx.uncook(t)));
substs.push_back(expr_ref_vector(mgr));
if (t.is_quantifier() && t.is_quantifier_forall()) {
int bound = t.get_quantifier_num_bound();
std::vector<sort> sorts;
std::vector<symbol> names;
hash_map<int,expr> subst;
for(int j = 0; j < bound; j++){
sort the_sort = t.get_quantifier_bound_sort(j);
symbol name = t.get_quantifier_bound_name(j);
expr skolem = ctx.constant(symbol(ctx,name),sort(ctx,the_sort));
expr val = tree->Eval(&edge,skolem);
expr_ref thing(ctx.uncook(val),mgr);
substs[0].push_back(thing);
expr local_skolem = tree->Localize(&edge,skolem);
(*local_func_decls).insert(local_skolem.decl());
}
}
svector<std::pair<unsigned, unsigned> > pos;
for(unsigned i = 0; i < edge.Children.size(); i++){
if(!tree->Empty(edge.Children[i])){
pos.push_back(std::pair<unsigned,unsigned>(i+1,0));
proof_ref prem = extract_proof(d,tree,edge.Children[i]);
prems.push_back(prem);
substs.push_back(expr_ref_vector(mgr));
}
}
func_decl f = node.Name;
std::vector<expr> args;
for(unsigned i = 0; i < edge.F.IndParams.size(); i++)
args.push_back(tree->Eval(&edge,edge.F.IndParams[i]));
expr conc = f(args);
::vector< ::proof *> pprems;
for(unsigned i = 0; i < prems.size(); i++)
pprems.push_back(prems[i].get());
proof_ref res(mgr.mk_hyper_resolve(pprems.size(),&pprems[0], ctx.uncook(conc), pos, substs),mgr);
return res;
}
proof_ref dl_interface::get_proof() {
if(_d->status == StatusRefutation){
hash_set<func_decl> locals;
local_func_decls = &locals;
return extract_proof(this,_d->cex.get_tree(),_d->cex.get_root());
}
else
return proof_ref(m_ctx.get_manager());
}
}

80
src/muz/duality/duality_dl_interface.h
View file

@ -1,80 +0,0 @@
/*++
Copyright (c) 2013 Microsoft Corporation
Module Name:
duality_dl_interface.h
Abstract:
SMT2 interface for Duality
Author:
Krystof Hoder (t-khoder) 2011-9-22.
Modified by Ken McMIllan (kenmcmil) 2013-4-18.
Revision History:
--*/
#ifndef DUALITY_DL_INTERFACE_H_
#define DUALITY_DL_INTERFACE_H_
#include "util/lbool.h"
#include "muz/base/dl_rule.h"
#include "muz/base/dl_rule_set.h"
#include "muz/base/dl_engine_base.h"
#include "util/statistics.h"
namespace datalog {
class context;
}
namespace Duality {
class duality_data;
class dl_interface : public datalog::engine_base {
duality_data *_d;
datalog::context &m_ctx;
public:
dl_interface(datalog::context& ctx);
~dl_interface() override;
lbool query(expr* query) override;
void cancel() override;
void cleanup() override;
void display_certificate(std::ostream& out) const override;
void collect_statistics(statistics& st) const override;
void reset_statistics() override;
expr_ref get_answer() override;
unsigned get_num_levels(func_decl* pred) override;
expr_ref get_cover_delta(int level, func_decl* pred) override;
void add_cover(int level, func_decl* pred, expr* property) override;
void updt_params() override;
model_ref get_model() override;
proof_ref get_proof() override;
duality_data *dd(){return _d;}
private:
void display_certificate_non_const(std::ostream& out);
};
}
#endif

1
src/muz/fp/CMakeLists.txt
View file

@ -8,7 +8,6 @@ z3_add_component(fp
bmc
clp
ddnf
duality_intf
muz
pdr
rel

3
src/muz/fp/dl_register_engine.cpp
View file

@ -23,7 +23,6 @@ Revision History:
#include "muz/rel/rel_context.h"
#include "muz/pdr/pdr_dl_interface.h"
#include "muz/ddnf/ddnf.h"
#include "muz/duality/duality_dl_interface.h"
#include "muz/spacer/spacer_dl_interface.h"
namespace datalog {
@ -45,8 +44,6 @@ namespace datalog {
return alloc(tab, *m_ctx);
case CLP_ENGINE:
return alloc(clp, *m_ctx);
case DUALITY_ENGINE:
return alloc(Duality::dl_interface, *m_ctx);
case DDNF_ENGINE:
return alloc(ddnf, *m_ctx);
case LAST_ENGINE:

1
src/smt/smt_internalizer.cpp
View file

@ -611,7 +611,6 @@ namespace smt {
case OP_XOR:
UNREACHABLE();
case OP_OEQ:
case OP_INTERP:
UNREACHABLE();
default:
break;