mirror of
https://github.com/Z3Prover/z3
synced 2025-04-23 17:15:31 +00:00
more work on interpolation
This commit is contained in:
Ken McMillan
parent
d66211c007
commit
ae9276ad9b
12 changed files with 978 additions and 21 deletions
|
|
@ -33,6 +33,11 @@ Revision History:
|
|||
#include"smt_implied_equalities.h"
|
||||
#include"iz3interp.h"
|
||||
#include"iz3profiling.h"
|
||||
#include"iz3hash.h"
|
||||
|
||||
#ifndef WIN32
|
||||
using namespace stl_ext;
|
||||
#endif
|
||||
|
||||
typedef interpolation_options_struct *Z3_interpolation_options;
|
||||
|
||||
|
|
@ -40,7 +45,7 @@ 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, "PROOF", "true");
|
||||
Z3_set_param_value(cfg, "MODEL", "true");
|
||||
Z3_set_param_value(cfg, "PRE_SIMPLIFIER","false");
|
||||
Z3_set_param_value(cfg, "SIMPLIFY_CLAUSES","false");
|
||||
|
|
@ -69,7 +74,7 @@ extern "C" {
|
|||
pre_cnsts_vec[i] = a;
|
||||
}
|
||||
|
||||
vector<int> pre_parents_vec; // get parents in a vector
|
||||
::vector<int> pre_parents_vec; // get parents in a vector
|
||||
if(parents){
|
||||
pre_parents_vec.resize(num);
|
||||
for(int i = 0; i < num; i++)
|
||||
|
|
@ -109,7 +114,7 @@ extern "C" {
|
|||
Z3_ast *interps,
|
||||
Z3_model *model,
|
||||
Z3_literals *labels,
|
||||
bool incremental,
|
||||
int incremental,
|
||||
int num_theory,
|
||||
Z3_ast *theory
|
||||
){
|
||||
|
|
@ -198,4 +203,242 @@ extern "C" {
|
|||
opts->map[name] = value;
|
||||
}
|
||||
|
||||
|
||||
|
||||
};
|
||||
|
||||
|
||||
static void tokenize(const std::string &str, std::vector<std::string> &tokens){
|
||||
for(unsigned i = 0; i < str.size();){
|
||||
if(str[i] == ' '){i++; continue;}
|
||||
unsigned beg = i;
|
||||
while(i < str.size() && str[i] != ' ')i++;
|
||||
if(i > beg)
|
||||
tokens.push_back(str.substr(beg,i-beg));
|
||||
}
|
||||
}
|
||||
|
||||
static void get_file_params(const char *filename, hash_map<std::string,std::string> ¶ms){
|
||||
std::ifstream f(filename);
|
||||
if(f){
|
||||
std::string first_line;
|
||||
std::getline(f,first_line);
|
||||
// std::cout << "first line: '" << first_line << "'" << std::endl;
|
||||
if(first_line.size() >= 2 && first_line[0] == ';' && first_line[1] == '!'){
|
||||
std::vector<std::string> tokens;
|
||||
tokenize(first_line.substr(2,first_line.size()-2),tokens);
|
||||
for(unsigned i = 0; i < tokens.size(); i++){
|
||||
std::string &tok = tokens[i];
|
||||
int eqpos = tok.find('=');
|
||||
if(eqpos >= 0 && eqpos < (int)tok.size()){
|
||||
std::string left = tok.substr(0,eqpos);
|
||||
std::string right = tok.substr(eqpos+1,tok.size()-eqpos-1);
|
||||
params[left] = right;
|
||||
}
|
||||
}
|
||||
}
|
||||
f.close();
|
||||
}
|
||||
}
|
||||
|
||||
extern "C" {
|
||||
|
||||
static void iZ3_write_seq(Z3_context ctx, int num, Z3_ast *cnsts, const char *filename, int num_theory, Z3_ast *theory){
|
||||
int num_fmlas = num+num_theory;
|
||||
std::vector<Z3_ast> fmlas(num_fmlas);
|
||||
if(num_theory)
|
||||
std::copy(theory,theory+num_theory,fmlas.begin());
|
||||
for(int i = 0; i < num_theory; i++)
|
||||
fmlas[i] = Z3_mk_implies(ctx,Z3_mk_true(ctx),fmlas[i]);
|
||||
std::copy(cnsts,cnsts+num,fmlas.begin()+num_theory);
|
||||
Z3_string smt = Z3_benchmark_to_smtlib_string(ctx,"none","AUFLIA","unknown","",num_fmlas-1,&fmlas[0],fmlas[num_fmlas-1]);
|
||||
std::ofstream f(filename);
|
||||
if(num_theory)
|
||||
f << ";! THEORY=" << num_theory << "\n";
|
||||
f << smt;
|
||||
f.close();
|
||||
}
|
||||
|
||||
void Z3_write_interpolation_problem(Z3_context ctx, int num, Z3_ast *cnsts, int *parents, const char *filename, int num_theory, Z3_ast *theory){
|
||||
if(!parents){
|
||||
iZ3_write_seq(ctx,num,cnsts,filename,num_theory,theory);
|
||||
return;
|
||||
}
|
||||
std::vector<Z3_ast> tcnsts(num);
|
||||
hash_map<int,Z3_ast> syms;
|
||||
for(int j = 0; j < num - 1; j++){
|
||||
std::ostringstream oss;
|
||||
oss << "$P" << j;
|
||||
std::string name = oss.str();
|
||||
Z3_symbol s = Z3_mk_string_symbol(ctx, name.c_str());
|
||||
Z3_ast symbol = Z3_mk_const(ctx, s, Z3_mk_bool_sort(ctx));
|
||||
syms[j] = symbol;
|
||||
tcnsts[j] = Z3_mk_implies(ctx,cnsts[j],symbol);
|
||||
}
|
||||
tcnsts[num-1] = Z3_mk_implies(ctx,cnsts[num-1],Z3_mk_false(ctx));
|
||||
for(int j = num-2; j >= 0; j--){
|
||||
int parent = parents[j];
|
||||
// assert(parent >= 0 && parent < num);
|
||||
tcnsts[parent] = Z3_mk_implies(ctx,syms[j],tcnsts[parent]);
|
||||
}
|
||||
iZ3_write_seq(ctx,num,&tcnsts[0],filename,num_theory,theory);
|
||||
}
|
||||
|
||||
static std::vector<Z3_ast> read_cnsts;
|
||||
static std::vector<int> read_parents;
|
||||
static std::ostringstream read_error;
|
||||
static std::string read_msg;
|
||||
static std::vector<Z3_ast> read_theory;
|
||||
|
||||
static bool iZ3_parse(Z3_context ctx, const char *filename, const char **error, std::vector<Z3_ast> &assertions){
|
||||
read_error.clear();
|
||||
try {
|
||||
std::string foo(filename);
|
||||
if(!foo.empty() && foo[foo.size()-1] == '2'){
|
||||
Z3_ast ass = Z3_parse_smtlib2_file(ctx, filename, 0, 0, 0, 0, 0, 0);
|
||||
Z3_app app = Z3_to_app(ctx,ass);
|
||||
int nconjs = Z3_get_app_num_args(ctx,app);
|
||||
assertions.resize(nconjs);
|
||||
for(int k = 0; k < nconjs; k++)
|
||||
assertions[k] = Z3_get_app_arg(ctx,app,k);
|
||||
}
|
||||
else {
|
||||
Z3_parse_smtlib_file(ctx, filename, 0, 0, 0, 0, 0, 0);
|
||||
int numa = Z3_get_smtlib_num_assumptions(ctx);
|
||||
int numf = Z3_get_smtlib_num_formulas(ctx);
|
||||
int num = numa + numf;
|
||||
|
||||
assertions.resize(num);
|
||||
for(int j = 0; j < num; j++){
|
||||
if(j < numa)
|
||||
assertions[j] = Z3_get_smtlib_assumption(ctx,j);
|
||||
else
|
||||
assertions[j] = Z3_get_smtlib_formula(ctx,j-numa);
|
||||
}
|
||||
}
|
||||
}
|
||||
catch(...) {
|
||||
read_error << "SMTLIB parse error: " << Z3_get_smtlib_error(ctx);
|
||||
read_msg = read_error.str();
|
||||
*error = read_msg.c_str();
|
||||
return false;
|
||||
}
|
||||
Z3_set_error_handler(ctx, 0);
|
||||
return true;
|
||||
}
|
||||
|
||||
|
||||
int Z3_read_interpolation_problem(Z3_context ctx, int *_num, Z3_ast **cnsts, int **parents, const char *filename, const char **error, int *ret_num_theory, Z3_ast **theory ){
|
||||
|
||||
hash_map<std::string,std::string> file_params;
|
||||
get_file_params(filename,file_params);
|
||||
|
||||
int num_theory = 0;
|
||||
if(file_params.find("THEORY") != file_params.end())
|
||||
num_theory = atoi(file_params["THEORY"].c_str());
|
||||
|
||||
std::vector<Z3_ast> assertions;
|
||||
if(!iZ3_parse(ctx,filename,error,assertions))
|
||||
return false;
|
||||
|
||||
if(num_theory > (int)assertions.size())
|
||||
num_theory = assertions.size();
|
||||
int num = assertions.size() - num_theory;
|
||||
|
||||
read_cnsts.resize(num);
|
||||
read_parents.resize(num);
|
||||
read_theory.resize(num_theory);
|
||||
|
||||
for(int j = 0; j < num_theory; j++)
|
||||
read_theory[j] = assertions[j];
|
||||
for(int j = 0; j < num; j++)
|
||||
read_cnsts[j] = assertions[j+num_theory];
|
||||
|
||||
if(ret_num_theory)
|
||||
*ret_num_theory = num_theory;
|
||||
if(theory)
|
||||
*theory = &read_theory[0];
|
||||
|
||||
if(!parents){
|
||||
*_num = num;
|
||||
*cnsts = &read_cnsts[0];
|
||||
return true;
|
||||
}
|
||||
|
||||
for(int j = 0; j < num; j++)
|
||||
read_parents[j] = SHRT_MAX;
|
||||
|
||||
hash_map<Z3_ast,int> pred_map;
|
||||
|
||||
for(int j = 0; j < num; j++){
|
||||
Z3_ast lhs = 0, rhs = read_cnsts[j];
|
||||
|
||||
if(Z3_get_decl_kind(ctx,Z3_get_app_decl(ctx,Z3_to_app(ctx,rhs))) == Z3_OP_IMPLIES){
|
||||
Z3_app app1 = Z3_to_app(ctx,rhs);
|
||||
Z3_ast lhs1 = Z3_get_app_arg(ctx,app1,0);
|
||||
Z3_ast rhs1 = Z3_get_app_arg(ctx,app1,1);
|
||||
if(Z3_get_decl_kind(ctx,Z3_get_app_decl(ctx,Z3_to_app(ctx,lhs1))) == Z3_OP_AND){
|
||||
Z3_app app2 = Z3_to_app(ctx,lhs1);
|
||||
int nconjs = Z3_get_app_num_args(ctx,app2);
|
||||
for(int k = nconjs - 1; k >= 0; --k)
|
||||
rhs1 = Z3_mk_implies(ctx,Z3_get_app_arg(ctx,app2,k),rhs1);
|
||||
rhs = rhs1;
|
||||
}
|
||||
}
|
||||
|
||||
while(1){
|
||||
Z3_app app = Z3_to_app(ctx,rhs);
|
||||
Z3_func_decl func = Z3_get_app_decl(ctx,app);
|
||||
Z3_decl_kind dk = Z3_get_decl_kind(ctx,func);
|
||||
if(dk == Z3_OP_IMPLIES){
|
||||
if(lhs){
|
||||
Z3_ast child = lhs;
|
||||
if(pred_map.find(child) == pred_map.end()){
|
||||
read_error << "formula " << j+1 << ": unknown: " << Z3_ast_to_string(ctx,child);
|
||||
goto fail;
|
||||
}
|
||||
int child_num = pred_map[child];
|
||||
if(read_parents[child_num] != SHRT_MAX){
|
||||
read_error << "formula " << j+1 << ": multiple reference: " << Z3_ast_to_string(ctx,child);
|
||||
goto fail;
|
||||
}
|
||||
read_parents[child_num] = j;
|
||||
}
|
||||
lhs = Z3_get_app_arg(ctx,app,0);
|
||||
rhs = Z3_get_app_arg(ctx,app,1);
|
||||
}
|
||||
else {
|
||||
if(!lhs){
|
||||
read_error << "formula " << j+1 << ": should be (implies {children} fmla parent)";
|
||||
goto fail;
|
||||
}
|
||||
read_cnsts[j] = lhs;
|
||||
Z3_ast name = rhs;
|
||||
if(pred_map.find(name) != pred_map.end()){
|
||||
read_error << "formula " << j+1 << ": duplicate symbol";
|
||||
goto fail;
|
||||
}
|
||||
pred_map[name] = j;
|
||||
break;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
for(int j = 0; j < num-1; j++)
|
||||
if(read_parents[j] == SHRT_MIN){
|
||||
read_error << "formula " << j+1 << ": unreferenced";
|
||||
goto fail;
|
||||
}
|
||||
|
||||
*_num = num;
|
||||
*cnsts = &read_cnsts[0];
|
||||
*parents = &read_parents[0];
|
||||
return true;
|
||||
|
||||
fail:
|
||||
read_msg = read_error.str();
|
||||
*error = read_msg.c_str();
|
||||
return false;
|
||||
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -7750,8 +7750,6 @@ END_MLAPI_EXCLUDE
|
|||
are considered to have global scope (i.e., may appear in any
|
||||
interpolant formula).
|
||||
|
||||
def_API('Z3_interpolate', INT, (_in(CONTEXT), _in(INT), _in_array(1,AST), _in_array(1,UINT), _in(PARAMS), _out_array(1,AST), _out(MODEL), _out(LITERALS), _in(BOOL), _in(INT), _in_array(9,AST),))
|
||||
|
||||
|
||||
*/
|
||||
|
||||
|
|
@ -7762,11 +7760,11 @@ END_MLAPI_EXCLUDE
|
|||
__in_ecount(num) unsigned *parents,
|
||||
__in Z3_params options,
|
||||
__out_ecount(num-1) Z3_ast *interps,
|
||||
__out Z3_model *model = 0,
|
||||
__out Z3_literals *labels = 0,
|
||||
__in bool incremental = false,
|
||||
__in int num_theory = 0,
|
||||
__in_ecount(num_theory) Z3_ast *theory = 0);
|
||||
__out Z3_model *model,
|
||||
__out Z3_literals *labels,
|
||||
__in int incremental,
|
||||
__in int num_theory,
|
||||
__in_ecount(num_theory) Z3_ast *theory);
|
||||
|
||||
/** Return a string summarizing cumulative time used for
|
||||
interpolation. This string is purely for entertainment purposes
|
||||
|
|
@ -7779,6 +7777,49 @@ END_MLAPI_EXCLUDE
|
|||
|
||||
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)
|
||||
|
||||
Returns true on success.
|
||||
|
||||
File formats: Currently two formats are supported, based on
|
||||
SMT-LIB2. For sequence interpolants, the sequence of constraints is
|
||||
represented by the sequence of "assert" commands in the file.
|
||||
|
||||
For tree interpolants, one symbol of type bool is associated to
|
||||
each vertex of the tree. For each vertex v there is an "assert"
|
||||
of the form:
|
||||
|
||||
(implies (and c1 ... cn f) v)
|
||||
|
||||
where c1 .. cn are the children of v (which must precede v in the file)
|
||||
and f is the formula assiciated to node v. The last formula in the
|
||||
file is the root vertex, and is represented by the predicate "false".
|
||||
|
||||
A solution to a tree interpolation problem can be thought of as a
|
||||
valuation of the vertices that makes all the implications true
|
||||
where each value is represented using the common symbols between
|
||||
the formulas in the subtree and the remainder of the formulas.
|
||||
*/
|
||||
|
||||
|
||||
int Z3_API
|
||||
Z3_read_interpolation_problem(__in Z3_context ctx,
|
||||
__out int *num,
|
||||
__out_ecount(*num) Z3_ast **cnsts,
|
||||
__out_ecount(*num) int **parents,
|
||||
__in const char *filename,
|
||||
__out const char **error,
|
||||
__out int *num_theory,
|
||||
__out_ecount(*num_theory) Z3_ast **theory);
|
||||
|
||||
|
||||
|
||||
#endif
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue