mirror of
https://github.com/Z3Prover/z3
synced 2025-04-23 17:15:31 +00:00
more work on incorporating iz3
This commit is contained in:
Ken McMillan
parent
e5f5e008aa
commit
9792f6dd33
11 changed files with 2527 additions and 7 deletions
201
src/api/api_interp.cpp
Normal file
201
src/api/api_interp.cpp
Normal file
|
|
@ -0,0 +1,201 @@
|
|||
/*++
|
||||
Copyright (c) 2011 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
api_interp.cpp
|
||||
|
||||
Abstract:
|
||||
API for interpolation
|
||||
|
||||
Author:
|
||||
|
||||
Ken McMillan
|
||||
|
||||
Revision History:
|
||||
|
||||
--*/
|
||||
#include<iostream>
|
||||
#include"z3.h"
|
||||
#include"api_log_macros.h"
|
||||
#include"api_context.h"
|
||||
#include"api_tactic.h"
|
||||
#include"api_solver.h"
|
||||
#include"api_model.h"
|
||||
#include"api_stats.h"
|
||||
#include"api_ast_vector.h"
|
||||
#include"tactic2solver.h"
|
||||
#include"scoped_ctrl_c.h"
|
||||
#include"cancel_eh.h"
|
||||
#include"scoped_timer.h"
|
||||
#include"smt_strategic_solver.h"
|
||||
#include"smt_solver.h"
|
||||
#include"smt_implied_equalities.h"
|
||||
#include"iz3interp.h"
|
||||
#include"iz3profiling.h"
|
||||
|
||||
typedef interpolation_options_struct *Z3_interpolation_options;
|
||||
|
||||
extern "C" {
|
||||
|
||||
Z3_context Z3_mk_interpolation_context(Z3_config cfg){
|
||||
if(!cfg) cfg = Z3_mk_config();
|
||||
Z3_set_param_value(cfg, "PROOF_MODE", "2");
|
||||
Z3_set_param_value(cfg, "MODEL", "true");
|
||||
Z3_set_param_value(cfg, "PRE_SIMPLIFIER","false");
|
||||
Z3_set_param_value(cfg, "SIMPLIFY_CLAUSES","false");
|
||||
|
||||
Z3_context ctx = Z3_mk_context(cfg);
|
||||
Z3_del_config(cfg);
|
||||
return ctx;
|
||||
}
|
||||
|
||||
void Z3_interpolate_proof(Z3_context ctx,
|
||||
Z3_ast proof,
|
||||
int num,
|
||||
Z3_ast *cnsts,
|
||||
int *parents,
|
||||
Z3_interpolation_options options,
|
||||
Z3_ast *interps,
|
||||
int num_theory,
|
||||
Z3_ast *theory
|
||||
){
|
||||
|
||||
if(num > 1){ // if we have interpolants to compute
|
||||
|
||||
ptr_vector<ast> pre_cnsts_vec(num); // get constraints in a vector
|
||||
for(int i = 0; i < num; i++){
|
||||
ast *a = to_ast(cnsts[i]);
|
||||
pre_cnsts_vec[i] = a;
|
||||
}
|
||||
|
||||
vector<int> pre_parents_vec; // get parents in a vector
|
||||
if(parents){
|
||||
pre_parents_vec.resize(num);
|
||||
for(int i = 0; i < num; i++)
|
||||
pre_parents_vec[i] = parents[i];
|
||||
}
|
||||
|
||||
ptr_vector<ast> theory_vec; // get background theory in a vector
|
||||
if(theory){
|
||||
theory_vec.resize(num_theory);
|
||||
for(int i = 0; i < num_theory; i++)
|
||||
theory_vec[i] = to_ast(theory[i]);
|
||||
}
|
||||
|
||||
ptr_vector<ast> interpolants(num-1); // make space for result
|
||||
|
||||
scoped_ptr<ast_manager> _m(&mk_c(ctx)->m());
|
||||
iz3interpolate(_m,
|
||||
to_ast(proof),
|
||||
pre_cnsts_vec,
|
||||
pre_parents_vec,
|
||||
interpolants,
|
||||
theory_vec,
|
||||
(interpolation_options) options);
|
||||
|
||||
// copy result back
|
||||
for(unsigned i = 0; i < interpolants.size(); i++)
|
||||
interps[i] = of_ast(interpolants[i]);
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
Z3_lbool Z3_interpolate(Z3_context ctx,
|
||||
int num,
|
||||
Z3_ast *cnsts,
|
||||
int *parents,
|
||||
Z3_interpolation_options options,
|
||||
Z3_ast *interps,
|
||||
Z3_model *model,
|
||||
Z3_literals *labels,
|
||||
bool incremental,
|
||||
int num_theory,
|
||||
Z3_ast *theory
|
||||
){
|
||||
|
||||
|
||||
if(!incremental){
|
||||
|
||||
profiling::timer_start("Z3 assert");
|
||||
|
||||
Z3_push(ctx); // so we can rewind later
|
||||
|
||||
for(int i = 0; i < num; i++)
|
||||
Z3_assert_cnstr(ctx,cnsts[i]); // assert all the constraints
|
||||
|
||||
if(theory){
|
||||
for(int i = 0; i < num_theory; i++)
|
||||
Z3_assert_cnstr(ctx,theory[i]);
|
||||
}
|
||||
|
||||
profiling::timer_stop("Z3 assert");
|
||||
}
|
||||
|
||||
|
||||
// Get a proof of unsat
|
||||
|
||||
Z3_ast proof;
|
||||
Z3_lbool result;
|
||||
|
||||
profiling::timer_start("Z3 solving");
|
||||
result = Z3_check_assumptions(ctx, 0, 0, model, &proof, 0, 0);
|
||||
profiling::timer_stop("Z3 solving");
|
||||
|
||||
switch (result) {
|
||||
case Z3_L_FALSE:
|
||||
|
||||
Z3_interpolate_proof(ctx,
|
||||
proof,
|
||||
num,
|
||||
cnsts,
|
||||
parents,
|
||||
options,
|
||||
interps,
|
||||
num_theory,
|
||||
theory);
|
||||
break;
|
||||
|
||||
case Z3_L_UNDEF:
|
||||
if(labels)
|
||||
*labels = Z3_get_relevant_labels(ctx);
|
||||
break;
|
||||
|
||||
case Z3_L_TRUE:
|
||||
if(labels)
|
||||
*labels = Z3_get_relevant_labels(ctx);
|
||||
break;
|
||||
}
|
||||
|
||||
return result;
|
||||
|
||||
}
|
||||
|
||||
static std::string Z3_profile_string;
|
||||
|
||||
Z3_string Z3_interpolation_profile(Z3_context ctx){
|
||||
std::ostringstream f;
|
||||
profiling::print(f);
|
||||
Z3_profile_string = f.str();
|
||||
return Z3_profile_string.c_str();
|
||||
}
|
||||
|
||||
|
||||
Z3_interpolation_options
|
||||
Z3_mk_interpolation_options(){
|
||||
return (Z3_interpolation_options) new interpolation_options_struct;
|
||||
}
|
||||
|
||||
void
|
||||
Z3_del_interpolation_options(Z3_interpolation_options opts){
|
||||
delete opts;
|
||||
}
|
||||
|
||||
void
|
||||
Z3_set_interpolation_option(Z3_interpolation_options opts,
|
||||
Z3_string name,
|
||||
Z3_string value){
|
||||
opts->map[name] = value;
|
||||
}
|
||||
|
||||
};
|
||||
122
src/api/z3_api.h
122
src/api/z3_api.h
|
|
@ -7660,6 +7660,128 @@ END_MLAPI_EXCLUDE
|
|||
|
||||
/*@}*/
|
||||
|
||||
/**
|
||||
@name Interpolation
|
||||
*/
|
||||
/*@{*/
|
||||
|
||||
/** \brief This function generates a Z3 context suitable for generation of
|
||||
interpolants. Formulas can be generated as abstract syntx trees in
|
||||
this context using the Z3 C API.
|
||||
|
||||
Interpolants are also generated as AST's in this context.
|
||||
|
||||
If cfg is non-null, it will be used as the base configuration
|
||||
for the Z3 context. This makes it possible to set Z3 options
|
||||
to be used during interpolation. This feature should be used
|
||||
with some caution however, as it may be that certain Z3 options
|
||||
are incompatible with interpolation.
|
||||
|
||||
def_API('Z3_mk_interpolation_context', CONTEXT, (_in(CONFIG),))
|
||||
|
||||
*/
|
||||
|
||||
Z3_context Z3_API Z3_mk_interpolation_context(__in Z3_config cfg);
|
||||
|
||||
|
||||
/** Constant reprepresenting a root of a formula tree for tree interpolation */
|
||||
#define IZ3_ROOT SHRT_MAX
|
||||
|
||||
/** This function uses Z3 to determine satisfiability of a set of
|
||||
constraints. If UNSAT, an interpolant is returned, based on the
|
||||
refutation generated by Z3. If SAT, a model is returned.
|
||||
|
||||
If "parents" is non-null, computes a tree interpolant. The tree is
|
||||
defined by the array "parents". This array maps each formula in
|
||||
the tree to its parent, where formulas are indicated by their
|
||||
integer index in "cnsts". The parent of formula n must have index
|
||||
greater than n. The last formula is the root of the tree. Its
|
||||
parent entry should be the constant IZ3_ROOT.
|
||||
|
||||
If "parents" is null, computes a sequence interpolant.
|
||||
|
||||
\param ctx The Z3 context. Must be generated by iz3_mk_context
|
||||
\param num The number of constraints in the sequence
|
||||
\param cnsts Array of constraints (AST's in context ctx)
|
||||
\param parents The parents vector defining the tree structure
|
||||
\param options Interpolation options (may be NULL)
|
||||
\param interps Array to return interpolants (size at least num-1, may be NULL)
|
||||
\param model Returns a Z3 model if constraints SAT (may be NULL)
|
||||
\param labels Returns relevant labels if SAT (may be NULL)
|
||||
\param incremental
|
||||
|
||||
VERY IMPORTANT: All the Z3 formulas in cnsts must be in Z3
|
||||
context ctx. The model and interpolants returned are also
|
||||
in this context.
|
||||
|
||||
The return code is as in Z3_check_assumptions, that is,
|
||||
|
||||
Z3_L_FALSE = constraints UNSAT (interpolants returned)
|
||||
Z3_L_TRUE = constraints SAT (model returned)
|
||||
Z3_L_UNDEF = Z3 produced no result, or interpolation not possible
|
||||
|
||||
Currently, this function supports integer and boolean variables,
|
||||
as well as arrays over these types, with linear arithmetic,
|
||||
uninterpreted functions and quantifiers over integers (that is
|
||||
AUFLIA). Interpolants are produced in AUFLIA. However, some
|
||||
uses of array operations may cause quantifiers to appear in the
|
||||
interpolants even when there are no quantifiers in the input formulas.
|
||||
Although quantifiers may appear in the input formulas, Z3 may give up in
|
||||
this case, returning Z3_L_UNDEF.
|
||||
|
||||
If "incremental" is true, cnsts must contain exactly the set of
|
||||
formulas that are currently asserted in the context. If false,
|
||||
there must be no formulas currently asserted in the context.
|
||||
Setting "incremental" to true makes it posisble to incrementally
|
||||
add and remove constraints from the context until the context
|
||||
becomes UNSAT, at which point an interpolant is computed. Caution
|
||||
must be used, however. Before popping the context, if you wish to
|
||||
keep the interolant formulas, you *must* preserve them by using
|
||||
Z3_persist_ast. Also, if you want to simplify the interpolant
|
||||
formulas using Z3_simplify, you must first pop all of the
|
||||
assertions in the context (or use a different context). Otherwise,
|
||||
the formulas will be simplified *relative* to these constraints,
|
||||
which is almost certainly not what you want.
|
||||
|
||||
|
||||
Current limitations on tree interpolants. In a tree interpolation
|
||||
problem, each constant (0-ary function symbol) must occur only
|
||||
along one path from root to leaf. Function symbols (of arity > 0)
|
||||
are considered to have global scope (i.e., may appear in any
|
||||
interpolant formula).
|
||||
|
||||
def_API('Z3_interpolate', LBOOL, (_in(CONTEXT),), (_in(INT),), (_in_ptr(AST),),
|
||||
(_in_ptr(INT),), (_in(PARAMS),), (_in_ptr(AST),),
|
||||
(_out(MODEL),), (_out(LITERALS),), (_in(BOOL),), (_in(INT),), (_in_ptr(AST,0),))
|
||||
|
||||
*/
|
||||
|
||||
|
||||
Z3_lbool Z3_API Z3_interpolate(Z3_context ctx,
|
||||
int num,
|
||||
Z3_ast *cnsts,
|
||||
int *parents,
|
||||
Z3_interpolation_options options,
|
||||
Z3_ast *interps,
|
||||
Z3_model *model = 0,
|
||||
Z3_literals *labels = 0,
|
||||
bool incremental = false,
|
||||
int num_theory = 0,
|
||||
Z3_ast *theory = 0);
|
||||
|
||||
/** 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);
|
||||
|
||||
|
||||
|
||||
#endif
|
||||
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue