mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 05:18:44 +00:00
Code Activity

Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-04-17 16:10:13 +01:00
parent f1a1267d4c af444beb2e
commit 7e6ab736c0
38 changed files with 20225 additions and 20225 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

146
src/api/api_interp.cpp
View file

@ -1,20 +1,20 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Copyright (c) 2011 Microsoft Corporation
Module Name:
Module Name:
api_interp.cpp
api_interp.cpp
Abstract:
API for interpolation
Abstract:
API for interpolation
Author:
Author:
Ken McMillan
Ken McMillan
Revision History:
Revision History:
--*/
--*/
#include<iostream>
#include<sstream>
#include<vector>
@ -191,19 +191,19 @@ extern "C" {
Z3_interpolation_options
Z3_mk_interpolation_options(){
Z3_mk_interpolation_options(){
return (Z3_interpolation_options) new interpolation_options_struct;
}
void
Z3_del_interpolation_options(Z3_interpolation_options opts){
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){
Z3_set_interpolation_option(Z3_interpolation_options opts,
Z3_string name,
Z3_string value){
opts->map[name] = value;
}
@ -412,11 +412,11 @@ extern "C" {
Z3_ast foo = Z3_mk_interpolant(ctx, and_vec(ctx, c));
chs[parents[i]].push_back(foo);
}
{
svector<Z3_ast> &c = chs[num - 1];
c.push_back(cnsts[num - 1]);
res = and_vec(ctx, c);
}
{
svector<Z3_ast> &c = chs[num - 1];
c.push_back(cnsts[num - 1]);
res = and_vec(ctx, c);
}
}
Z3_inc_ref(ctx, res);
return res;
@ -620,8 +620,8 @@ extern "C" {
for (unsigned j = 0; j < num - 1; j++)
if (read_parents[j] == SHRT_MAX){
read_error << "formula " << j + 1 << ": unreferenced";
goto fail;
read_error << "formula " << j + 1 << ": unreferenced";
goto fail;
}
*_num = num;
@ -643,69 +643,69 @@ extern "C" {
#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.
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 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.
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
\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.
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,
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
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 AULIA. 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.
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 AULIA. 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.
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).
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', BOOL, (_in(CONTEXT), _in(UINT), _in_array(1, AST), _in_array(1, UINT), _in(PARAMS), _out_array(1, AST), _out(MODEL), _out(LITERALS), _in(UINT), _in(UINT), _in_array(9, AST)))
def_API('Z3_interpolate', BOOL, (_in(CONTEXT), _in(UINT), _in_array(1, AST), _in_array(1, UINT), _in(PARAMS), _out_array(1, AST), _out(MODEL), _out(LITERALS), _in(UINT), _in(UINT), _in_array(9, AST)))
*/
Z3_lbool Z3_API Z3_interpolate(__in Z3_context ctx,

258
src/cmd_context/interpolant_cmds.cpp
View file

@ -1,20 +1,20 @@
/*++
Copyright (c) 2013 Microsoft Corporation
Copyright (c) 2013 Microsoft Corporation
Module Name:
Module Name:
interpolant_cmds.cpp
interpolant_cmds.cpp
Abstract:
Commands for interpolation.
Abstract:
Commands for interpolation.
Author:
Author:
Leonardo (leonardo) 2011-12-23
Leonardo (leonardo) 2011-12-23
Notes:
Notes:
--*/
--*/
#include<sstream>
#include"cmd_context.h"
#include"cmd_util.h"
@ -43,180 +43,180 @@ static void show_interpolant_and_maybe_check(cmd_context & ctx,
bool check)
{
if (m_params.get_bool("som", false))
m_params.set_bool("flat", true);
th_rewriter s(ctx.m(), m_params);
if (m_params.get_bool("som", false))
m_params.set_bool("flat", true);
th_rewriter s(ctx.m(), m_params);
for(unsigned i = 0; i < interps.size(); i++){
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);
expr_ref r(ctx.m());
proof_ref pr(ctx.m());
s(to_expr(interps[i]),r,pr);
ctx.regular_stream() << mk_pp(r.get(), ctx.m()) << std::endl;
ctx.regular_stream() << mk_pp(r.get(), ctx.m()) << std::endl;
#if 0
ast_smt_pp pp(ctx.m());
pp.set_logic(ctx.get_logic().str().c_str());
pp.display_smt2(ctx.regular_stream(), to_expr(interps[i]));
ctx.regular_stream() << std::endl;
ast_smt_pp pp(ctx.m());
pp.set_logic(ctx.get_logic().str().c_str());
pp.display_smt2(ctx.regular_stream(), to_expr(interps[i]));
ctx.regular_stream() << std::endl;
#endif
}
}
s.cleanup();
s.cleanup();
// verify, for the paranoid...
if(check || interp_params(m_params).check()){
std::ostringstream err;
ast_manager &_m = ctx.m();
// 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());
// 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";
}
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]);
}
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());
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)");
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);
check_can_interpolate(ctx);
// get the proof, if there is one
// 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");
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
// 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;
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
// compute an interpolant
ptr_vector<ast> interps;
ptr_vector<ast> interps;
try {
iz3interpolate(ctx.m(),pr.get(),cnsts,t,interps,0);
}
catch (iz3_bad_tree &) {
throw cmd_exception("interpolation pattern contains non-asserted formula");
}
catch (iz3_incompleteness &) {
throw cmd_exception("incompleteness in interpolator");
}
try {
iz3interpolate(ctx.m(),pr.get(),cnsts,t,interps,0);
}
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);
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);
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);
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_FINE);
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());
// 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_FINE);
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;
ptr_vector<ast> cnsts;
ptr_vector<ast> interps;
model_ref m;
// compute an interpolant
// compute an interpolant
lbool res;
try {
res = iz3interpolate(_m, *sp.get(), t, cnsts, interps, m, 0);
}
catch (iz3_incompleteness &) {
throw cmd_exception("incompleteness in interpolator");
}
lbool res;
try {
res = iz3interpolate(_m, *sp.get(), t, cnsts, interps, m, 0);
}
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;
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_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;
}
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]);
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;
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 *foo = make_tree(ctx,exprs);
ctx.m().inc_ref(foo);
get_interpolant(ctx,foo,m_params);
ctx.m().dec_ref(foo);
expr *foo = make_tree(ctx,exprs);
ctx.m().inc_ref(foo);
get_interpolant(ctx,foo,m_params);
ctx.m().dec_ref(foo);
}
static void compute_interpolant(cmd_context & ctx, const ptr_vector<expr> &exprs, params_ref &m_params) {
expr *foo = make_tree(ctx, exprs);
ctx.m().inc_ref(foo);
compute_interpolant_and_maybe_check(ctx,foo,m_params,false);
ctx.m().dec_ref(foo);
expr *foo = make_tree(ctx, exprs);
ctx.m().inc_ref(foo);
compute_interpolant_and_maybe_check(ctx,foo,m_params,false);
ctx.m().dec_ref(foo);
}
@ -249,11 +249,11 @@ public:
}
virtual void set_next_arg(cmd_context & ctx, expr * arg) {
m_targets.push_back(arg);
m_targets.push_back(arg);
}
virtual void execute(cmd_context & ctx) {
get_interpolant(ctx,m_targets,m_params);
get_interpolant(ctx,m_targets,m_params);
}
};
@ -262,7 +262,7 @@ public:
compute_interpolant_cmd(char const * name = "compute-interpolant"):get_interpolant_cmd(name) {}
virtual void execute(cmd_context & ctx) {
compute_interpolant(ctx,m_targets,m_params);
compute_interpolant(ctx,m_targets,m_params);
}
};

18
src/cmd_context/interpolant_cmds.h
View file

@ -1,20 +1,20 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Copyright (c) 2011 Microsoft Corporation
Module Name:
Module Name:
interpolant_cmds.h
interpolant_cmds.h
Abstract:
Commands for interpolation.
Abstract:
Commands for interpolation.
Author:
Author:
Leonardo (leonardo) 2011-12-23
Leonardo (leonardo) 2011-12-23
Notes:
Notes:
--*/
--*/
#ifndef _INTERPOLANT_CMDS_H_
#define _INTERPOLANT_CMDS_H_

1782
src/duality/duality.h
View file

File diff suppressed because it is too large Load diff

194
src/duality/duality_profiling.cpp
View file

@ -1,22 +1,22 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Copyright (c) 2011 Microsoft Corporation
Module Name:
Module Name:
duality_profiling.cpp
duality_profiling.cpp
Abstract:
Abstract:
collection performance information for duality
collection performance information for duality
Author:
Author:
Ken McMillan (kenmcmil)
Ken McMillan (kenmcmil)
Revision History:
Revision History:
--*/
--*/
#include <map>
@ -36,109 +36,109 @@ Revision History:
namespace Duality {
void show_time(){
output_time(std::cout,current_time());
std::cout << "\n";
}
void show_time(){
output_time(std::cout,current_time());
std::cout << "\n";
}
typedef std::map<const char*, struct node> nmap;
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;
struct node {
std::string name;
clock_t time;
clock_t start_time;
nmap sub;
struct node *parent;
node();
} top;
node();
} top;
node::node(){
time = 0;
parent = 0;
}
struct node *current;
struct init {
init(){
top.name = "TOTAL";
current = &top;
node::node(){
time = 0;
parent = 0;
}
} initializer;
struct time_entry {
clock_t t;
time_entry(){t = 0;};
void add(clock_t incr){t += incr;}
};
struct node *current;
struct ltstr
{
bool operator()(const char* s1, const char* s2) const
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
{
return strcmp(s1, s2) < 0;
}
};
bool operator()(const char* s1, const char* s2) const
{
return strcmp(s1, s2) < 0;
}
};
typedef std::map<const char*, time_entry, ltstr> tmap;
typedef std::map<const char*, time_entry, ltstr> tmap;
static std::ostream *pfs;
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;
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);
}
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;
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;
}
child.start_time = current_time();
current = &child;
}
void timer_stop(const char *name){
if (current->name != name || !current->parent) {
void timer_stop(const char *name){
if (current->name != name || !current->parent) {
#if 0
std::cerr << "imbalanced timer_start and timer_stop";
exit(1);
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;
}
// 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;
}
}

34
src/duality/duality_profiling.h
View file

@ -1,22 +1,22 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Copyright (c) 2011 Microsoft Corporation
Module Name:
Module Name:
duality_profiling.h
duality_profiling.h
Abstract:
Abstract:
collection performance information for duality
collection performance information for duality
Author:
Author:
Ken McMillan (kenmcmil)
Ken McMillan (kenmcmil)
Revision History:
Revision History:
--*/
--*/
#ifndef DUALITYPROFILING_H
#define DUALITYPROFILING_H
@ -24,14 +24,14 @@ Revision History:
#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();
/** 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

8014
src/duality/duality_rpfp.cpp
View file

File diff suppressed because it is too large Load diff

6106
src/duality/duality_solver.cpp
View file

File diff suppressed because it is too large Load diff

1252
src/duality/duality_wrapper.cpp
View file

File diff suppressed because it is too large Load diff

1166
src/duality/duality_wrapper.h
View file

File diff suppressed because it is too large Load diff

80
src/interp/foci2.h
View file

@ -1,21 +1,21 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Copyright (c) 2011 Microsoft Corporation
Module Name:
Module Name:
foci2.h
foci2.h
Abstract:
Abstract:
An interface class for foci2.
An interface class for foci2.
Author:
Author:
Ken McMillan (kenmcmil)
Ken McMillan (kenmcmil)
Revision History:
Revision History:
--*/
--*/
#ifndef FOCI2_H
#define FOCI2_H
@ -31,45 +31,45 @@ Revision History:
class foci2 {
public:
virtual ~foci2(){}
virtual ~foci2(){}
typedef int ast;
typedef int symb;
typedef int ast;
typedef int symb;
/** Built-in operators */
enum ops {
And = 0, Or, Not, Iff, Ite, Equal, Plus, Times, Floor, Leq, Div, Bool, Int, Array, Tsym, Fsym, Forall, Exists, Distinct, LastOp
};
/** Built-in operators */
enum ops {
And = 0, Or, Not, Iff, Ite, Equal, Plus, Times, Floor, Leq, Div, Bool, Int, Array, Tsym, Fsym, Forall, Exists, Distinct, LastOp
};
virtual symb mk_func(const std::string &s) = 0;
virtual symb mk_pred(const std::string &s) = 0;
virtual ast mk_op(ops op, const std::vector<ast> args) = 0;
virtual ast mk_op(ops op, ast) = 0;
virtual ast mk_op(ops op, ast, ast) = 0;
virtual ast mk_op(ops op, ast, ast, ast) = 0;
virtual ast mk_int(const std::string &) = 0;
virtual ast mk_rat(const std::string &) = 0;
virtual ast mk_true() = 0;
virtual ast mk_false() = 0;
virtual ast mk_app(symb,const std::vector<ast> args) = 0;
virtual symb mk_func(const std::string &s) = 0;
virtual symb mk_pred(const std::string &s) = 0;
virtual ast mk_op(ops op, const std::vector<ast> args) = 0;
virtual ast mk_op(ops op, ast) = 0;
virtual ast mk_op(ops op, ast, ast) = 0;
virtual ast mk_op(ops op, ast, ast, ast) = 0;
virtual ast mk_int(const std::string &) = 0;
virtual ast mk_rat(const std::string &) = 0;
virtual ast mk_true() = 0;
virtual ast mk_false() = 0;
virtual ast mk_app(symb,const std::vector<ast> args) = 0;
virtual bool get_func(ast, symb &) = 0;
virtual bool get_pred(ast, symb &) = 0;
virtual bool get_op(ast, ops &) = 0;
virtual bool get_true(ast id) = 0;
virtual bool get_false(ast id) = 0;
virtual bool get_int(ast id, std::string &res) = 0;
virtual bool get_rat(ast id, std::string &res) = 0;
virtual const std::string &get_symb(symb) = 0;
virtual bool get_func(ast, symb &) = 0;
virtual bool get_pred(ast, symb &) = 0;
virtual bool get_op(ast, ops &) = 0;
virtual bool get_true(ast id) = 0;
virtual bool get_false(ast id) = 0;
virtual bool get_int(ast id, std::string &res) = 0;
virtual bool get_rat(ast id, std::string &res) = 0;
virtual const std::string &get_symb(symb) = 0;
virtual int get_num_args(ast) = 0;
virtual ast get_arg(ast, int) = 0;
virtual int get_num_args(ast) = 0;
virtual ast get_arg(ast, int) = 0;
virtual void show_ast(ast) = 0;
virtual void show_ast(ast) = 0;
virtual bool interpolate(const std::vector<ast> &frames, std::vector<ast> &itps, std::vector<int> parents) = 0;
virtual bool interpolate(const std::vector<ast> &frames, std::vector<ast> &itps, std::vector<int> parents) = 0;
FOCI2_EXPORT static foci2 *create(const std::string &);
FOCI2_EXPORT static foci2 *create(const std::string &);
};
#endif

494
src/interp/iz3base.cpp
View file

@ -1,22 +1,22 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Copyright (c) 2011 Microsoft Corporation
Module Name:
Module Name:
iz3base.cpp
iz3base.cpp
Abstract:
Abstract:
Base class for interpolators. Includes an AST manager and a scoping
object as bases.
Base class for interpolators. Includes an AST manager and a scoping
object as bases.
Author:
Author:
Ken McMillan (kenmcmil)
Ken McMillan (kenmcmil)
Revision History:
Revision History:
--*/
--*/
#ifdef _WINDOWS
#pragma warning(disable:4996)
@ -38,256 +38,256 @@ using namespace stl_ext;
iz3base::range &iz3base::ast_range(ast t){
return ast_ranges_hash[t].rng;
return ast_ranges_hash[t].rng;
}
iz3base::range &iz3base::sym_range(symb d){
return sym_range_hash[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)));
}
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;
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;
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();
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);
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);
}
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);
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;
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();
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]);
}
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);
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;
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);
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(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]);
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;
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;
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;
}
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);
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();
::solver *m_solver = (*sf)(m(), p, true, true, true, ::symbol::null);
::solver &s = *m_solver;
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();
::solver *m_solver = (*sf)(m(), p, true, true, true, ::symbol::null);
::solver &s = *m_solver;
for(unsigned i = 0; i < q.size(); i++)
s.assert_expr(to_expr(q[i].raw()));
lbool res = s.check_sat(0,0);
if(res == l_false){
::ast *proof = s.get_proof();
_proof = cook(proof);
}
else if(vars.size()) {
model_ref(_m);
s.get_model(_m);
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());
for(unsigned i = 0; i < q.size(); i++)
s.assert_expr(to_expr(q[i].raw()));
lbool res = s.check_sat(0,0);
if(res == l_false){
::ast *proof = s.get_proof();
_proof = cook(proof);
}
}
dealloc(m_solver);
return res != l_false;
else if(vars.size()) {
model_ref(_m);
s.get_model(_m);
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());
}
}
dealloc(m_solver);
return res != l_false;
}
@ -300,39 +300,39 @@ void iz3base::find_children(const stl_ext::hash_set<ast> &cnsts_set,
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]);
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);
}
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);
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]);
}
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,
@ -343,23 +343,23 @@ void iz3base::to_parents_vec_representation(const std::vector<ast> &_cnsts,
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;
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
// 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]);
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]);
}

242
src/interp/iz3base.h
View file

@ -1,22 +1,22 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Copyright (c) 2011 Microsoft Corporation
Module Name:
Module Name:
iz3base.h
iz3base.h
Abstract:
Abstract:
Base class for interpolators. Includes an AST manager and a scoping
object as bases.
Base class for interpolators. Includes an AST manager and a scoping
object as bases.
Author:
Author:
Ken McMillan (kenmcmil)
Ken McMillan (kenmcmil)
Revision History:
Revision History:
--*/
--*/
#ifndef IZ3BASE_H
#define IZ3BASE_H
@ -25,13 +25,13 @@ Revision History:
#include "iz3scopes.h"
namespace hash_space {
template <>
class hash<func_decl *> {
public:
size_t operator()(func_decl * const &s) const {
return (size_t) s;
}
};
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
@ -41,152 +41,152 @@ 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 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 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);
/** 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)? */
/** Is an expression local (in scope in some frame)? */
bool is_local(ast node){
return !range_is_empty(ast_scope(node));
}
bool is_local(ast node){
return !range_is_empty(ast_scope(node));
}
/** Simplify an expression */
/** Simplify an expression */
ast simplify(ast);
ast simplify(ast);
/** Constructor */
/** Constructor */
iz3base(ast_manager &_m_manager,
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;
}
: iz3mgr(_m_manager), scopes(_parents) {
initialize(_cnsts,_parents,_theory);
weak = false;
}
iz3base(const iz3mgr& other,
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;
}
: iz3mgr(other), scopes(_parents) {
initialize(_cnsts,_parents,_theory);
weak = false;
}
iz3base(const iz3mgr& other,
const std::vector<std::vector<ast> > &_cnsts,
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;
}
: iz3mgr(other), scopes(_parents) {
initialize(_cnsts,_parents,_theory);
weak = false;
}
iz3base(const iz3mgr& other)
: iz3mgr(other), scopes() {
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;
}
/* 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;}
/* Are we doing weak interpolants? */
bool weak_mode(){return weak;}
/** Print interpolation problem to an SMTLIB format file */
void print(const std::string &filename);
/** 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);
/** 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);
/** 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 "no interpolator";
}
/** Interpolator for clauses, to be implemented */
virtual void interpolate_clause(std::vector<ast> &lits, std::vector<ast> &itps){
throw "no interpolator";
}
ast get_proof_check_assump(range &rng){
std::vector<ast> cs(theory);
cs.push_back(cnsts[rng.hi]);
return make(And,cs);
}
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 "unknown assertion";
return it->second;
}
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 "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
);
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;
std::vector<ast> cnsts;
std::vector<ast> theory;
private:
struct ranges {
range rng;
range scp;
bool scope_computed;
ranges(){scope_computed = false;}
};
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
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
// int frames; // number of frames
protected:
void add_frame_range(int frame, ast t);
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<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);
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;
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;
};

276
src/interp/iz3checker.cpp
View file

@ -1,21 +1,21 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Copyright (c) 2011 Microsoft Corporation
Module Name:
Module Name:
iz3checker.cpp
iz3checker.cpp
Abstract:
Abstract:
check correctness of interpolant
check correctness of interpolant
Author:
Author:
Ken McMillan (kenmcmil)
Ken McMillan (kenmcmil)
Revision History:
Revision History:
--*/
--*/
#ifdef _WINDOWS
#pragma warning(disable:4996)
@ -40,154 +40,154 @@ 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 interpoaltion is
fixed, we can tree function symbols the same as constant symbols. */
/* 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 interpoaltion is
fixed, we can tree function symbols the same as constant symbols. */
bool is_tree;
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);
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);
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:;
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){
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);
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-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,0);
if(result != l_false){
err << "interpolant " << i << " is incorrect";
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,0);
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,0);
if(result != l_false)
err << "interpolant " << i << " is not implied by its downeard closurn";
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,0);
if(result != l_false)
err << "interpolant " << i << " is not implied by its downeard closurn";
return false;
}
s->pop(1);
}
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);
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;
}
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){
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;
std::vector<int> pos_map;
// convert to the parents vector representation
// convert to the parents vector representation
to_parents_vec_representation(_cnsts, tree, cnsts, parents, theory, pos_map);
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);
}
//use the parents vector representation to compute interpolant
return check(s,err,cnsts,parents,itp,theory);
}
iz3checker(ast_manager &_m)
: iz3base(_m) {
}
iz3checker(ast_manager &_m)
: iz3base(_m) {
}
iz3checker(iz3mgr &_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;
std::vector<T> _v(v.size());
for(unsigned i = 0; i < v.size(); i++)
_v[i] = v[i];
return _v;
}
@ -199,8 +199,8 @@ bool iz3check(ast_manager &_m_manager,
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));
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,
@ -211,8 +211,8 @@ bool iz3check(iz3mgr &mgr,
const std::vector<iz3mgr::ast> &interps,
const std::vector<iz3mgr::ast> &theory)
{
iz3checker chk(mgr);
return chk.check(s,err,cnsts,parents,interps,theory);
iz3checker chk(mgr);
return chk.check(s,err,cnsts,parents,interps,theory);
}
bool iz3check(ast_manager &_m_manager,
@ -222,6 +222,6 @@ bool iz3check(ast_manager &_m_manager,
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));
iz3checker chk(_m_manager);
return chk.check(s,err,chk.cook(_cnsts),chk.cook(tree),chk.cook(interps));
}

18
src/interp/iz3checker.h
View file

@ -1,21 +1,21 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Copyright (c) 2011 Microsoft Corporation
Module Name:
Module Name:
iz3checker.h
iz3checker.h
Abstract:
Abstract:
check correctness of an interpolant
check correctness of an interpolant
Author:
Author:
Ken McMillan (kenmcmil)
Ken McMillan (kenmcmil)
Revision History:
Revision History:
--*/
--*/
#ifndef IZ3_CHECKER_H
#define IZ3_CHECKER_H

638
src/interp/iz3foci.cpp
View file

@ -1,21 +1,21 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Copyright (c) 2011 Microsoft Corporation
Module Name:
Module Name:
iz3foci.cpp
iz3foci.cpp
Abstract:
Abstract:
Implements a secondary solver using foci2.
Implements a secondary solver using foci2.
Author:
Author:
Ken McMillan (kenmcmil)
Ken McMillan (kenmcmil)
Revision History:
Revision History:
--*/
--*/
#include <sstream>
#include <iostream>
@ -29,329 +29,329 @@ using namespace stl_ext;
class iz3foci_impl : public iz3secondary {
int frames;
int *parents;
foci2 *foci;
foci2::symb select_op;
foci2::symb store_op;
foci2::symb mod_op;
int frames;
int *parents;
foci2 *foci;
foci2::symb select_op;
foci2::symb store_op;
foci2::symb mod_op;
public:
iz3foci_impl(iz3mgr *mgr, int _frames, int *_parents) : iz3secondary(*mgr) {
frames = _frames;
parents = _parents;
foci = 0;
}
typedef hash_map<ast,foci2::ast> AstToNode;
AstToNode ast_to_node; // maps Z3 ast's to foci expressions
typedef hash_map<foci2::ast,ast> NodeToAst;
NodeToAst node_to_ast; // maps Z3 ast's to foci expressions
// We only use this for FuncDeclToSymbol, which has no range destructor
struct symb_hash {
size_t operator()(const symb &s) const {
return (size_t) s;
}
};
typedef hash_map<symb,foci2::symb> FuncDeclToSymbol;
FuncDeclToSymbol func_decl_to_symbol; // maps Z3 func decls to symbols
typedef hash_map<foci2::symb,symb> SymbolToFuncDecl;
SymbolToFuncDecl symbol_to_func_decl; // maps symbols to Z3 func decls
int from_symb(symb func){
std::string name = string_of_symbol(func);
bool is_bool = is_bool_type(get_range_type(func));
foci2::symb f;
if(is_bool)
f = foci->mk_pred(name);
else
f = foci->mk_func(name);
symbol_to_func_decl[f] = func;
func_decl_to_symbol[func] = f;
return f;
}
// create a symbol corresponding to a DeBruijn index of a particular type
// the type has to be encoded into the name because the same index can
// occur with different types
foci2::symb make_deBruijn_symbol(int index, type ty){
std::ostringstream s;
// s << "#" << index << "#" << type;
return foci->mk_func(s.str());
}
int from_Z3_ast(ast t){
std::pair<ast,foci2::ast> foo(t,0);
std::pair<AstToNode::iterator, bool> bar = ast_to_node.insert(foo);
int &res = bar.first->second;
if(!bar.second) return res;
int nargs = num_args(t);
std::vector<foci2::ast> args(nargs);
for(int i = 0; i < nargs; i++)
args[i] = from_Z3_ast(arg(t,i));
switch(op(t)){
case True:
res = foci->mk_true(); break;
case False:
res = foci->mk_false(); break;
case And:
res = foci->mk_op(foci2::And,args); break;
case Or:
res = foci->mk_op(foci2::Or,args); break;
case Not:
res = foci->mk_op(foci2::Not,args[0]); break;
case Iff:
res = foci->mk_op(foci2::Iff,args); break;
case OP_OEQ: // bit of a mystery, this one...
if(args[0] == args[1]) res = foci->mk_true();
else res = foci->mk_op(foci2::Iff,args);
break;
case Ite:
if(is_bool_type(get_type(t)))
res = foci->mk_op(foci2::And,foci->mk_op(foci2::Or,foci->mk_op(foci2::Not,args[0]),args[1]),foci->mk_op(foci2::Or,args[0],args[2]));
else
res = foci->mk_op(foci2::Ite,args);
break;
case Equal:
res = foci->mk_op(foci2::Equal,args); break;
case Implies:
args[0] = foci->mk_op(foci2::Not,args[0]); res = foci->mk_op(foci2::Or,args); break;
case Xor:
res = foci->mk_op(foci2::Not,foci->mk_op(foci2::Iff,args)); break;
case Leq:
res = foci->mk_op(foci2::Leq,args); break;
case Geq:
std::swap(args[0],args[1]); res = foci->mk_op(foci2::Leq,args); break;
case Gt:
res = foci->mk_op(foci2::Not,foci->mk_op(foci2::Leq,args)); break;
case Lt:
std::swap(args[0],args[1]); res = foci->mk_op(foci2::Not,foci->mk_op(foci2::Leq,args)); break;
case Plus:
res = foci->mk_op(foci2::Plus,args); break;
case Sub:
args[1] = foci->mk_op(foci2::Times,foci->mk_int("-1"),args[1]); res = foci->mk_op(foci2::Plus,args); break;
case Uminus:
res = foci->mk_op(foci2::Times,foci->mk_int("-1"),args[0]); break;
case Times:
res = foci->mk_op(foci2::Times,args); break;
case Idiv:
res = foci->mk_op(foci2::Div,args); break;
case Mod:
res = foci->mk_app(mod_op,args); break;
case Select:
res = foci->mk_app(select_op,args); break;
case Store:
res = foci->mk_app(store_op,args); break;
case Distinct:
res = foci->mk_op(foci2::Distinct,args); break;
case Uninterpreted: {
symb func = sym(t);
FuncDeclToSymbol::iterator it = func_decl_to_symbol.find(func);
foci2::symb f = (it == func_decl_to_symbol.end()) ? from_symb(func) : it->second;
if(foci->get_symb(f).substr(0,3) == "lbl" && args.size()==1) // HACK to handle Z3 labels
res = args[0];
else if(foci->get_symb(f).substr(0,3) == "lbl" && args.size()==0) // HACK to handle Z3 labels
res = foci->mk_true();
else res = foci->mk_app(f,args);
break;
}
case Numeral: {
std::string s = string_of_numeral(t);
res = foci->mk_int(s);
break;
}
case Forall:
case Exists: {
bool is_forall = op(t) == Forall;
foci2::ops qop = is_forall ? foci2::Forall : foci2::Exists;
int bvs = get_quantifier_num_bound(t);
std::vector<int> foci_bvs(bvs);
for(int i = 0; i < bvs; i++){
std::string name = get_quantifier_bound_name(t,i);
//Z3_string name = Z3_get_symbol_string(ctx,sym);
// type ty = get_quantifier_bound_type(t,i);
foci2::symb f = foci->mk_func(name);
foci2::ast v = foci->mk_app(f,std::vector<foci2::ast>());
foci_bvs[i] = v;
}
foci2::ast body = from_Z3_ast(get_quantifier_body(t));
foci_bvs.push_back(body);
res = foci->mk_op(qop,foci_bvs);
node_to_ast[res] = t; // desperate
break;
}
case Variable: { // a deBruijn index
int index = get_variable_index_value(t);
type ty = get_type(t);
foci2::symb symbol = make_deBruijn_symbol(index,ty);
res = foci->mk_app(symbol,std::vector<foci2::ast>());
break;
}
default:
{
std::cerr << "iZ3: unsupported Z3 operator in expression\n ";
print_expr(std::cerr,t);
std::cerr << "\n";
assert(0 && "iZ3: unsupported Z3 operator");
}
}
return res;
}
// convert an expr to Z3 ast
ast to_Z3_ast(foci2::ast i){
std::pair<foci2::ast,ast> foo(i,ast());
std::pair<NodeToAst::iterator,bool> bar = node_to_ast.insert(foo);
if(!bar.second) return bar.first->second;
ast &res = bar.first->second;
if(i < 0){
res = mk_not(to_Z3_ast(-i));
return res;
iz3foci_impl(iz3mgr *mgr, int _frames, int *_parents) : iz3secondary(*mgr) {
frames = _frames;
parents = _parents;
foci = 0;
}
// get the arguments
unsigned n = foci->get_num_args(i);
std::vector<ast> args(n);
for(unsigned j = 0; j < n; j++)
args[j] = to_Z3_ast(foci->get_arg(i,j));
typedef hash_map<ast,foci2::ast> AstToNode;
AstToNode ast_to_node; // maps Z3 ast's to foci expressions
// handle operators
foci2::ops o;
foci2::symb f;
std::string nval;
if(foci->get_true(i))
res = mk_true();
else if(foci->get_false(i))
res = mk_false();
else if(foci->get_op(i,o)){
switch(o){
case foci2::And:
res = make(And,args); break;
case foci2::Or:
res = make(Or,args); break;
case foci2::Not:
res = mk_not(args[0]); break;
case foci2::Iff:
res = make(Iff,args[0],args[1]); break;
case foci2::Ite:
res = make(Ite,args[0],args[1],args[2]); break;
case foci2::Equal:
res = make(Equal,args[0],args[1]); break;
case foci2::Plus:
res = make(Plus,args); break;
case foci2::Times:
res = make(Times,args); break;
case foci2::Div:
res = make(Idiv,args[0],args[1]); break;
case foci2::Leq:
res = make(Leq,args[0],args[1]); break;
case foci2::Distinct:
res = make(Distinct,args);
break;
case foci2::Tsym:
res = mk_true();
break;
case foci2::Fsym:
res = mk_false();
break;
case foci2::Forall:
case foci2::Exists:
{
int nargs = n;
std::vector<ast> bounds(nargs-1);
for(int i = 0; i < nargs-1; i++)
bounds[i] = args[i];
opr oz = o == foci2::Forall ? Forall : Exists;
res = make_quant(oz,bounds,args[nargs-1]);
}
break;
default:
assert("unknown built-in op");
}
}
else if(foci->get_int(i,nval)){
res = make_int(nval);
}
else if(foci->get_func(i,f)){
if(f == select_op){
assert(n == 2);
res = make(Select,args[0],args[1]);
}
else if(f == store_op){
assert(n == 3);
res = make(Store,args[0],args[1],args[2]);
}
else if(f == mod_op){
assert(n == 2);
res = make(Mod,args[0],args[1]);
}
else {
std::pair<int,symb> foo(f,(symb)0);
std::pair<SymbolToFuncDecl::iterator,bool> bar = symbol_to_func_decl.insert(foo);
symb &func_decl = bar.first->second;
if(bar.second){
std::cout << "unknown function symbol:\n";
foci->show_ast(i);
assert(0);
typedef hash_map<foci2::ast,ast> NodeToAst;
NodeToAst node_to_ast; // maps Z3 ast's to foci expressions
// We only use this for FuncDeclToSymbol, which has no range destructor
struct symb_hash {
size_t operator()(const symb &s) const {
return (size_t) s;
}
res = make(func_decl,args);
}
}
else {
std::cerr << "iZ3: unknown FOCI expression kind\n";
assert(0 && "iZ3: unknown FOCI expression kind");
}
return res;
}
};
int interpolate(const std::vector<ast> &cnsts, std::vector<ast> &itps){
assert((int)cnsts.size() == frames);
std::string lia("lia");
typedef hash_map<symb,foci2::symb> FuncDeclToSymbol;
FuncDeclToSymbol func_decl_to_symbol; // maps Z3 func decls to symbols
typedef hash_map<foci2::symb,symb> SymbolToFuncDecl;
SymbolToFuncDecl symbol_to_func_decl; // maps symbols to Z3 func decls
int from_symb(symb func){
std::string name = string_of_symbol(func);
bool is_bool = is_bool_type(get_range_type(func));
foci2::symb f;
if(is_bool)
f = foci->mk_pred(name);
else
f = foci->mk_func(name);
symbol_to_func_decl[f] = func;
func_decl_to_symbol[func] = f;
return f;
}
// create a symbol corresponding to a DeBruijn index of a particular type
// the type has to be encoded into the name because the same index can
// occur with different types
foci2::symb make_deBruijn_symbol(int index, type ty){
std::ostringstream s;
// s << "#" << index << "#" << type;
return foci->mk_func(s.str());
}
int from_Z3_ast(ast t){
std::pair<ast,foci2::ast> foo(t,0);
std::pair<AstToNode::iterator, bool> bar = ast_to_node.insert(foo);
int &res = bar.first->second;
if(!bar.second) return res;
int nargs = num_args(t);
std::vector<foci2::ast> args(nargs);
for(int i = 0; i < nargs; i++)
args[i] = from_Z3_ast(arg(t,i));
switch(op(t)){
case True:
res = foci->mk_true(); break;
case False:
res = foci->mk_false(); break;
case And:
res = foci->mk_op(foci2::And,args); break;
case Or:
res = foci->mk_op(foci2::Or,args); break;
case Not:
res = foci->mk_op(foci2::Not,args[0]); break;
case Iff:
res = foci->mk_op(foci2::Iff,args); break;
case OP_OEQ: // bit of a mystery, this one...
if(args[0] == args[1]) res = foci->mk_true();
else res = foci->mk_op(foci2::Iff,args);
break;
case Ite:
if(is_bool_type(get_type(t)))
res = foci->mk_op(foci2::And,foci->mk_op(foci2::Or,foci->mk_op(foci2::Not,args[0]),args[1]),foci->mk_op(foci2::Or,args[0],args[2]));
else
res = foci->mk_op(foci2::Ite,args);
break;
case Equal:
res = foci->mk_op(foci2::Equal,args); break;
case Implies:
args[0] = foci->mk_op(foci2::Not,args[0]); res = foci->mk_op(foci2::Or,args); break;
case Xor:
res = foci->mk_op(foci2::Not,foci->mk_op(foci2::Iff,args)); break;
case Leq:
res = foci->mk_op(foci2::Leq,args); break;
case Geq:
std::swap(args[0],args[1]); res = foci->mk_op(foci2::Leq,args); break;
case Gt:
res = foci->mk_op(foci2::Not,foci->mk_op(foci2::Leq,args)); break;
case Lt:
std::swap(args[0],args[1]); res = foci->mk_op(foci2::Not,foci->mk_op(foci2::Leq,args)); break;
case Plus:
res = foci->mk_op(foci2::Plus,args); break;
case Sub:
args[1] = foci->mk_op(foci2::Times,foci->mk_int("-1"),args[1]); res = foci->mk_op(foci2::Plus,args); break;
case Uminus:
res = foci->mk_op(foci2::Times,foci->mk_int("-1"),args[0]); break;
case Times:
res = foci->mk_op(foci2::Times,args); break;
case Idiv:
res = foci->mk_op(foci2::Div,args); break;
case Mod:
res = foci->mk_app(mod_op,args); break;
case Select:
res = foci->mk_app(select_op,args); break;
case Store:
res = foci->mk_app(store_op,args); break;
case Distinct:
res = foci->mk_op(foci2::Distinct,args); break;
case Uninterpreted: {
symb func = sym(t);
FuncDeclToSymbol::iterator it = func_decl_to_symbol.find(func);
foci2::symb f = (it == func_decl_to_symbol.end()) ? from_symb(func) : it->second;
if(foci->get_symb(f).substr(0,3) == "lbl" && args.size()==1) // HACK to handle Z3 labels
res = args[0];
else if(foci->get_symb(f).substr(0,3) == "lbl" && args.size()==0) // HACK to handle Z3 labels
res = foci->mk_true();
else res = foci->mk_app(f,args);
break;
}
case Numeral: {
std::string s = string_of_numeral(t);
res = foci->mk_int(s);
break;
}
case Forall:
case Exists: {
bool is_forall = op(t) == Forall;
foci2::ops qop = is_forall ? foci2::Forall : foci2::Exists;
int bvs = get_quantifier_num_bound(t);
std::vector<int> foci_bvs(bvs);
for(int i = 0; i < bvs; i++){
std::string name = get_quantifier_bound_name(t,i);
//Z3_string name = Z3_get_symbol_string(ctx,sym);
// type ty = get_quantifier_bound_type(t,i);
foci2::symb f = foci->mk_func(name);
foci2::ast v = foci->mk_app(f,std::vector<foci2::ast>());
foci_bvs[i] = v;
}
foci2::ast body = from_Z3_ast(get_quantifier_body(t));
foci_bvs.push_back(body);
res = foci->mk_op(qop,foci_bvs);
node_to_ast[res] = t; // desperate
break;
}
case Variable: { // a deBruijn index
int index = get_variable_index_value(t);
type ty = get_type(t);
foci2::symb symbol = make_deBruijn_symbol(index,ty);
res = foci->mk_app(symbol,std::vector<foci2::ast>());
break;
}
default:
{
std::cerr << "iZ3: unsupported Z3 operator in expression\n ";
print_expr(std::cerr,t);
std::cerr << "\n";
assert(0 && "iZ3: unsupported Z3 operator");
}
}
return res;
}
// convert an expr to Z3 ast
ast to_Z3_ast(foci2::ast i){
std::pair<foci2::ast,ast> foo(i,ast());
std::pair<NodeToAst::iterator,bool> bar = node_to_ast.insert(foo);
if(!bar.second) return bar.first->second;
ast &res = bar.first->second;
if(i < 0){
res = mk_not(to_Z3_ast(-i));
return res;
}
// get the arguments
unsigned n = foci->get_num_args(i);
std::vector<ast> args(n);
for(unsigned j = 0; j < n; j++)
args[j] = to_Z3_ast(foci->get_arg(i,j));
// handle operators
foci2::ops o;
foci2::symb f;
std::string nval;
if(foci->get_true(i))
res = mk_true();
else if(foci->get_false(i))
res = mk_false();
else if(foci->get_op(i,o)){
switch(o){
case foci2::And:
res = make(And,args); break;
case foci2::Or:
res = make(Or,args); break;
case foci2::Not:
res = mk_not(args[0]); break;
case foci2::Iff:
res = make(Iff,args[0],args[1]); break;
case foci2::Ite:
res = make(Ite,args[0],args[1],args[2]); break;
case foci2::Equal:
res = make(Equal,args[0],args[1]); break;
case foci2::Plus:
res = make(Plus,args); break;
case foci2::Times:
res = make(Times,args); break;
case foci2::Div:
res = make(Idiv,args[0],args[1]); break;
case foci2::Leq:
res = make(Leq,args[0],args[1]); break;
case foci2::Distinct:
res = make(Distinct,args);
break;
case foci2::Tsym:
res = mk_true();
break;
case foci2::Fsym:
res = mk_false();
break;
case foci2::Forall:
case foci2::Exists:
{
int nargs = n;
std::vector<ast> bounds(nargs-1);
for(int i = 0; i < nargs-1; i++)
bounds[i] = args[i];
opr oz = o == foci2::Forall ? Forall : Exists;
res = make_quant(oz,bounds,args[nargs-1]);
}
break;
default:
assert("unknown built-in op");
}
}
else if(foci->get_int(i,nval)){
res = make_int(nval);
}
else if(foci->get_func(i,f)){
if(f == select_op){
assert(n == 2);
res = make(Select,args[0],args[1]);
}
else if(f == store_op){
assert(n == 3);
res = make(Store,args[0],args[1],args[2]);
}
else if(f == mod_op){
assert(n == 2);
res = make(Mod,args[0],args[1]);
}
else {
std::pair<int,symb> foo(f,(symb)0);
std::pair<SymbolToFuncDecl::iterator,bool> bar = symbol_to_func_decl.insert(foo);
symb &func_decl = bar.first->second;
if(bar.second){
std::cout << "unknown function symbol:\n";
foci->show_ast(i);
assert(0);
}
res = make(func_decl,args);
}
}
else {
std::cerr << "iZ3: unknown FOCI expression kind\n";
assert(0 && "iZ3: unknown FOCI expression kind");
}
return res;
}
int interpolate(const std::vector<ast> &cnsts, std::vector<ast> &itps){
assert((int)cnsts.size() == frames);
std::string lia("lia");
#ifdef _FOCI2
foci = foci2::create(lia);
foci = foci2::create(lia);
#else
foci = 0;
foci = 0;
#endif
if(!foci){
std::cerr << "iZ3: cannot find foci lia solver.\n";
assert(0);
if(!foci){
std::cerr << "iZ3: cannot find foci lia solver.\n";
assert(0);
}
select_op = foci->mk_func("select");
store_op = foci->mk_func("store");
mod_op = foci->mk_func("mod");
std::vector<foci2::ast> foci_cnsts(frames), foci_itps(frames-1), foci_parents;
if(parents)
foci_parents.resize(frames);
for(int i = 0; i < frames; i++){
foci_cnsts[i] = from_Z3_ast(cnsts[i]);
if(parents)
foci_parents[i] = parents[i];
}
int res = foci->interpolate(foci_cnsts, foci_itps, foci_parents);
if(res == 0){
assert((int)foci_itps.size() == frames-1);
itps.resize(frames-1);
for(int i = 0; i < frames-1; i++){
// foci->show_ast(foci_itps[i]);
itps[i] = to_Z3_ast(foci_itps[i]);
}
}
ast_to_node.clear();
node_to_ast.clear();
func_decl_to_symbol.clear();
symbol_to_func_decl.clear();
delete foci;
return res;
}
select_op = foci->mk_func("select");
store_op = foci->mk_func("store");
mod_op = foci->mk_func("mod");
std::vector<foci2::ast> foci_cnsts(frames), foci_itps(frames-1), foci_parents;
if(parents)
foci_parents.resize(frames);
for(int i = 0; i < frames; i++){
foci_cnsts[i] = from_Z3_ast(cnsts[i]);
if(parents)
foci_parents[i] = parents[i];
}
int res = foci->interpolate(foci_cnsts, foci_itps, foci_parents);
if(res == 0){
assert((int)foci_itps.size() == frames-1);
itps.resize(frames-1);
for(int i = 0; i < frames-1; i++){
// foci->show_ast(foci_itps[i]);
itps[i] = to_Z3_ast(foci_itps[i]);
}
}
ast_to_node.clear();
node_to_ast.clear();
func_decl_to_symbol.clear();
symbol_to_func_decl.clear();
delete foci;
return res;
}
};
iz3secondary *iz3foci::create(iz3mgr *mgr, int num, int *parents){
return new iz3foci_impl(mgr,num,parents);
return new iz3foci_impl(mgr,num,parents);
}

20
src/interp/iz3foci.h
View file

@ -1,21 +1,21 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Copyright (c) 2011 Microsoft Corporation
Module Name:
Module Name:
iz3foci.h
iz3foci.h
Abstract:
Abstract:
Implements a secondary solver using foci2.
Implements a secondary solver using foci2.
Author:
Author:
Ken McMillan (kenmcmil)
Ken McMillan (kenmcmil)
Revision History:
Revision History:
--*/
--*/
#ifndef IZ3FOCI_H
#define IZ3FOCI_H
@ -26,7 +26,7 @@ Revision History:
class iz3foci {
public:
static iz3secondary *create(iz3mgr *mgr, int num, int *parents);
static iz3secondary *create(iz3mgr *mgr, int num, int *parents);
};
#endif

732
src/interp/iz3hash.h
View file

@ -1,30 +1,30 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Copyright (c) 2011 Microsoft Corporation
Module Name:
Module Name:
iz3hash.h
iz3hash.h
Abstract:
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.
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.
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.
This package lives in namespace hash_space. Specializations of
class "hash" should be made in this namespace.
Author:
Author:
Ken McMillan (kenmcmil)
Ken McMillan (kenmcmil)
Revision History:
Revision History:
--*/
--*/
#ifndef IZ3_HASH_H
#define IZ3_HASH_H
@ -42,437 +42,437 @@ Revision History:
namespace hash_space {
template <typename T> class hash {};
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
template <>
class hash<int> {
public:
size_t operator()(const int &s) const {
return s;
}
};
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 hash<std::string> {
public:
size_t operator()(const std::string &s) const {
return string_hash(s.c_str(), s.size(), 0);
}
};
template<class Value, class Key, class HashFun, class GetKey, class KeyEqFun>
class hashtable
{
public:
template <>
class hash<std::pair<int,int> > {
public:
size_t operator()(const std::pair<int,int> &p) const {
return p.first + p.second;
}
};
typedef Value &reference;
typedef const Value &const_reference;
struct Entry
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
{
Entry* next;
Value val;
public:
typedef Value &reference;
typedef const Value &const_reference;
struct Entry
{
Entry* next;
Value val;
Entry(const Value &_val) : val(_val) {next = 0;}
};
Entry(const Value &_val) : val(_val) {next = 0;}
};
struct iterator
{
Entry* ent;
hashtable* tab;
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;
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(Entry* _ent, hashtable* _tab) : ent(_ent), tab(_tab) { }
iterator() { }
iterator() { }
Value &operator*() const { return ent->val; }
Value &operator*() const { return ent->val; }
Value *operator->() const { return &(operator*()); }
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++() {
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;
}
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;
}
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;
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;
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 Entry* _ent, const hashtable* _tab) : ent(_ent), tab(_tab) { }
const_iterator() { }
const_iterator() { }
const Value &operator*() const { return ent->val; }
const Value &operator*() const { return ent->val; }
const Value *operator->() const { return &(operator*()); }
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++() {
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;
}
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;
}
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;
typedef std::vector<Entry*> Table;
Table buckets;
size_t entries;
HashFun hash_fun ;
GetKey get_key;
KeyEqFun key_eq_fun;
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 *)0) {
entries = 0;
}
entries = 0;
}
hashtable(const hashtable& other) {
dup(other);
}
hashtable(const hashtable& other) {
dup(other);
}
hashtable& operator= (const hashtable& other) {
if (&other != this)
dup(other);
return *this;
}
hashtable& operator= (const hashtable& other) {
if (&other != this)
dup(other);
return *this;
}
~hashtable() {
clear();
}
~hashtable() {
clear();
}
size_t size() const {
return entries;
}
size_t size() const {
return entries;
}
bool empty() const {
return size() == 0;
}
bool empty() const {
return size() == 0;
}
void swap(hashtable& other) {
buckets.swap(other.buckets);
std::swap(entries, other.entries);
}
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 begin() {
for (size_t i = 0; i < buckets.size(); ++i)
if (buckets[i])
return iterator(buckets[i], this);
return end();
}
iterator end() {
return iterator(0, this);
}
iterator end() {
return iterator(0, 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 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(0, this);
}
const_iterator end() const {
return const_iterator(0, this);
}
size_t get_bucket(const Value& val, size_t n) const {
return hash_fun(get_key(val)) % n;
}
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_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());
}
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);
Entry *lookup(const Value& val, bool ins = false)
{
resize(entries + 1);
size_t n = get_bucket(val);
Entry* from = buckets[n];
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;
for (Entry* ent = from; ent; ent = ent->next)
if (key_eq_fun(get_key(ent->val), get_key(val)))
return ent;
if(!ins) return 0;
if(!ins) return 0;
Entry* tmp = new Entry(val);
tmp->next = from;
buckets[n] = tmp;
++entries;
return tmp;
}
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];
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;
for (Entry* ent = from; ent; ent = ent->next)
if (key_eq_fun(get_key(ent->val), key))
return ent;
return 0;
}
return 0;
}
const_iterator find(const Key& key) const {
return const_iterator(lookup_key(key),this);
}
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);
}
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);
}
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);
}
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;
}
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*)(0));
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 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*)(0));
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 != 0;) {
Entry* next = ent->next;
delete ent;
ent = next;
}
buckets[i] = 0;
}
entries = 0;
}
void clear()
{
for (size_t i = 0; i < buckets.size(); ++i) {
for (Entry* ent = buckets[i]; ent != 0;) {
Entry* next = ent->next;
delete ent;
ent = next;
}
buckets[i] = 0;
}
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;
}
};
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 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>
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 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> {
template <typename Element, class HashFun = hash<Element>,
class EqFun = equal<Element> >
class hash_set
: public hashtable<Element,Element,HashFun,identity<Element>,EqFun> {
public:
public:
typedef Element value_type;
typedef Element value_type;
hash_set()
: hashtable<Element,Element,HashFun,identity<Element>,EqFun>(7) {}
};
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> {
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:
public:
hash_map()
: hashtable<std::pair<Key,Value>,Key,HashFun,proj1<Key,Value>,EqFun>(7) {}
hash_map()
: hashtable<std::pair<Key,Value>,Key,HashFun,proj1<Key,Value>,EqFun>(7) {}
Value &operator[](const Key& key) {
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;
}
};
lookup(kvp,true)->val.second;
}
};
}
#endif

732
src/interp/iz3interp.cpp
View file

@ -1,21 +1,21 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Copyright (c) 2011 Microsoft Corporation
Module Name:
Module Name:
iz3interp.cpp
iz3interp.cpp
Abstract:
Abstract:
Interpolation based on proof translation.
Interpolation based on proof translation.
Author:
Author:
Ken McMillan (kenmcmil)
Ken McMillan (kenmcmil)
Revision History:
Revision History:
--*/
--*/
/* Copyright 2011 Microsoft Research. */
@ -52,96 +52,96 @@ using namespace stl_ext;
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;
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) {}
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;
}
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);
}
}
}
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);
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;
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]]++;
}
// if multiple children of a tree node are used, we can't delete it
std::vector<int> used_children;
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;
}
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];
}
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";
}
// 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]);
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
@ -149,20 +149,20 @@ struct frame_reducer {
frame_reducer(context _ctx){
}
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 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){
}
void fix_interpolants(std::vector<ast> &interpolants){
}
};
#endif
@ -170,236 +170,236 @@ struct frame_reducer {
#if 0
static lbool test_secondary(context ctx,
int num,
ast *cnsts,
ast *interps,
int *parents = 0
){
iz3secondary *sp = iz3foci::create(ctx,num,parents);
std::vector<ast> frames(num), interpolants(num-1);
std::copy(cnsts,cnsts+num,frames.begin());
int res = sp->interpolate(frames,interpolants);
if(res == 0)
int num,
ast *cnsts,
ast *interps,
int *parents = 0
){
iz3secondary *sp = iz3foci::create(ctx,num,parents);
std::vector<ast> frames(num), interpolants(num-1);
std::copy(cnsts,cnsts+num,frames.begin());
int res = sp->interpolate(frames,interpolants);
if(res == 0)
std::copy(interpolants.begin(),interpolants.end(),interps);
return res ? L_TRUE : L_FALSE;
return res ? L_TRUE : L_FALSE;
}
#endif
template<class T>
struct killme {
T *p;
killme(){p = 0;}
void set(T *_p) {p = _p;}
~killme(){
if(p)
delete p;
}
T *p;
killme(){p = 0;}
void set(T *_p) {p = _p;}
~killme(){
if(p)
delete p;
}
};
class iz3interp : public iz3base {
public:
killme<iz3secondary> sp_killer;
killme<iz3translation> tr_killer;
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;
}
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
){
int num = cnsts.size();
iz3secondary *sp = iz3foci::create(this,num,(int *)(parents.empty()?0:&parents[0]));
int res = sp->interpolate(cnsts, interps);
if(res != 0)
throw "secondary failed";
}
void test_secondary(const std::vector<ast> &cnsts,
const std::vector<int> &parents,
std::vector<ast> &interps
){
int num = cnsts.size();
iz3secondary *sp = iz3foci::create(this,num,(int *)(parents.empty()?0:&parents[0]));
int res = sp->interpolate(cnsts, interps);
if(res != 0)
throw "secondary failed";
}
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 = 0
){
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 = 0
){
#if 0
test_secondary(cnsts,parents,interps);
return;
test_secondary(cnsts,parents,interps);
return;
#endif
profiling::timer_start("Interpolation prep");
profiling::timer_start("Interpolation prep");
// get rid of frames not used in proof
// 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);
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);
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();
// if this is really a sequence problem, we can make it easier
if(is_linear(parents_vec))
parents_vec.clear();
// create a secondary prover
iz3secondary *sp = iz3foci::create(this,num,parents_vec.empty()?0:&parents_vec[0]);
sp_killer.set(sp); // kill this on exit
// create a secondary prover
iz3secondary *sp = iz3foci::create(this,num,parents_vec.empty()?0:&parents_vec[0]);
sp_killer.set(sp); // kill this on exit
#define BINARY_INTERPOLATION
#ifndef BINARY_INTERPOLATION
// create a translator
iz3translation *tr = iz3translation::create(*this,sp,cnsts_vec,parents_vec,theory);
tr_killer.set(tr);
// 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);
// 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);
// create a proof object to hold the translation
iz3proof pf(tr);
profiling::timer_stop("Interpolation prep");
profiling::timer_stop("Interpolation prep");
// translate into an interpolatable proof
profiling::timer_start("Proof translation");
tr->translate(proof,pf);
profiling::timer_stop("Proof translation");
// translate into an interpolatable proof
profiling::timer_start("Proof translation");
tr->translate(proof,pf);
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");
// 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);
iz3base the_base(*this,cnsts_vec,parents_vec,theory);
profiling::timer_stop("Interpolation prep");
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]);
}
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);
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);
// 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);
// create a proof object to hold the translation
iz3proof pf(tr);
// translate into an interpolatable proof
profiling::timer_start("Proof translation");
tr->translate(proof,pf);
profiling::timer_stop("Proof translation");
// translate into an interpolatable proof
profiling::timer_start("Proof translation");
tr->translate(proof,pf);
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");
}
// 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);
// put back in the removed frames
fr.fix_interpolants(interps_vec);
interps = 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 = 0
){
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 = 0
){
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 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 = 0
){
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 = 0
){
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 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()));
}
iz3interp(ast_manager &_m_manager)
: iz3base(_m_manager) {}
iz3interp(ast_manager &_m_manager)
: iz3base(_m_manager) {}
};
void iz3interpolate(ast_manager &_m_manager,
@ -410,24 +410,24 @@ void iz3interpolate(ast_manager &_m_manager,
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]);
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,
@ -438,25 +438,25 @@ void iz3interpolate(ast_manager &_m_manager,
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]);
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,
@ -466,19 +466,19 @@ void iz3interpolate(ast_manager &_m_manager,
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);
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]);
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);
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,
@ -489,40 +489,40 @@ lbool iz3interpolate(ast_manager &_m_manager,
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,0);
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;
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,0);
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);
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
@ -536,11 +536,11 @@ void interpolation_options_struct::apply(iz3base &b){
class iz3stack_unlimiter {
public:
iz3stack_unlimiter() {
struct rlimit rl = {RLIM_INFINITY, RLIM_INFINITY};
setrlimit(RLIMIT_STACK, &rl);
// nothing to be done if above fails
}
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

28
src/interp/iz3interp.h
View file

@ -1,21 +1,21 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Copyright (c) 2011 Microsoft Corporation
Module Name:
Module Name:
iz3interp.h
iz3interp.h
Abstract:
Abstract:
Interpolation based on proof translation.
Interpolation based on proof translation.
Author:
Author:
Ken McMillan (kenmcmil)
Ken McMillan (kenmcmil)
Revision History:
Revision History:
--*/
--*/
#ifndef IZ3_INTERP_H
#define IZ3_INTERP_H
@ -26,12 +26,12 @@ Revision History:
class iz3base;
struct interpolation_options_struct {
stl_ext::hash_map<std::string,std::string> map;
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);
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 */

1258
src/interp/iz3mgr.cpp
View file

File diff suppressed because it is too large Load diff

1246
src/interp/iz3mgr.h
View file

File diff suppressed because it is too large Load diff

218
src/interp/iz3pp.cpp
View file

@ -1,21 +1,21 @@
/*++
Copyright (c) 2013 Microsoft Corporation
Copyright (c) 2013 Microsoft Corporation
Module Name:
Module Name:
iz3pp.cpp
iz3pp.cpp
Abstract:
Abstract:
Pretty-print interpolation problems
Pretty-print interpolation problems
Author:
Author:
Ken McMillan (kenmcmil)
Ken McMillan (kenmcmil)
Revision History:
Revision History:
--*/
--*/
/* Copyright 2011 Microsoft Research. */
#include <assert.h>
@ -40,70 +40,70 @@ using namespace stl_ext;
// We promise not to use this for hash_map with range destructor
namespace stl_ext {
template <>
template <>
class hash<expr *> {
public:
size_t operator()(const expr *p) const {
return (size_t) p;
}
};
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;
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);
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; }
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;
}
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();
}
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) {}
iz3pp_helper(ast_manager &_m_manager)
: iz3mgr(_m_manager) {}
};
void iz3pp(ast_manager &m,
@ -111,75 +111,75 @@ void iz3pp(ast_manager &m,
expr *tree,
std::ostream& out) {
unsigned sz = cnsts_vec.size();
expr* const* cnsts = &cnsts_vec[0];
unsigned sz = cnsts_vec.size();
expr* const* cnsts = &cnsts_vec[0];
out << "(set-option :produce-interpolants true)\n";
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();
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);
smt2_pp_environment_dbg env(m);
for (unsigned i = 0; i < sz; ++i) {
expr* e = cnsts[i];
for_each_expr(visitor, visited, e);
}
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());
}
// 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();
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();
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 (; 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 (; 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);
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";
}
else {
out << nm;
}
out << ")";
out << "(check-sat)\n";
out << "(get-interpolant ";
iz3pp_helper pp(m);
pp.print_tree(pp.cook(tree),cnames,out);
out << ")\n";
}
out << "(check-sat)\n";
out << "(get-interpolant ";
iz3pp_helper pp(m);
pp.print_tree(pp.cook(tree),cnames,out);
out << ")\n";
}

18
src/interp/iz3pp.h
View file

@ -1,21 +1,21 @@
/*++
Copyright (c) 2013 Microsoft Corporation
Copyright (c) 2013 Microsoft Corporation
Module Name:
Module Name:
iz3pp.cpp
iz3pp.cpp
Abstract:
Abstract:
Pretty-print interpolation problems
Pretty-print interpolation problems
Author:
Author:
Ken McMillan (kenmcmil)
Ken McMillan (kenmcmil)
Revision History:
Revision History:
--*/
--*/
#ifndef IZ3_PP_H
#define IZ3_PP_H

188
src/interp/iz3profiling.cpp
View file

@ -1,21 +1,21 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Copyright (c) 2011 Microsoft Corporation
Module Name:
Module Name:
iz3profiling.h
iz3profiling.h
Abstract:
Abstract:
Some routines for measuring performance.
Some routines for measuring performance.
Author:
Author:
Ken McMillan (kenmcmil)
Ken McMillan (kenmcmil)
Revision History:
Revision History:
--*/
--*/
#ifdef _WINDOWS
#pragma warning(disable:4996)
@ -40,114 +40,114 @@ Revision History:
static double current_time()
{
static stopwatch sw;
static bool started = false;
if(!started){
sw.start();
started = true;
}
return sw.get_current_seconds();
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;
os << time;
}
namespace profiling {
void show_time(){
output_time(std::cout,current_time());
std::cout << "\n";
}
void show_time(){
output_time(std::cout,current_time());
std::cout << "\n";
}
typedef std::map<const char*, struct node> nmap;
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;
struct node {
std::string name;
clock_t time;
clock_t start_time;
nmap sub;
struct node *parent;
node();
} top;
node();
} top;
node::node(){
time = 0;
parent = 0;
}
struct node *current;
struct init {
init(){
top.name = "TOTAL";
current = &top;
node::node(){
time = 0;
parent = 0;
}
} initializer;
struct time_entry {
clock_t t;
time_entry(){t = 0;};
void add(clock_t incr){t += incr;}
};
struct node *current;
struct ltstr
{
bool operator()(const char* s1, const char* s2) const
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
{
return strcmp(s1, s2) < 0;
}
};
bool operator()(const char* s1, const char* s2) const
{
return strcmp(s1, s2) < 0;
}
};
typedef std::map<const char*, time_entry, ltstr> tmap;
typedef std::map<const char*, time_entry, ltstr> tmap;
static std::ostream *pfs;
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_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 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;
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;
}
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);
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;
}
current->time += (current_time() - current->start_time);
current = current->parent;
}
}

34
src/interp/iz3profiling.h
View file

@ -1,21 +1,21 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Copyright (c) 2011 Microsoft Corporation
Module Name:
Module Name:
iz3profiling.h
iz3profiling.h
Abstract:
Abstract:
Some routines for measuring performance.
Some routines for measuring performance.
Author:
Author:
Ken McMillan (kenmcmil)
Ken McMillan (kenmcmil)
Revision History:
Revision History:
--*/
--*/
#ifndef IZ3PROFILING_H
#define IZ3PROFILING_H
@ -23,14 +23,14 @@ Revision History:
#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();
/** 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

864
src/interp/iz3proof.cpp
View file

File diff suppressed because it is too large Load diff

352
src/interp/iz3proof.h
View file

@ -1,21 +1,21 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Copyright (c) 2011 Microsoft Corporation
Module Name:
Module Name:
iz3proof.h
iz3proof.h
Abstract:
Abstract:
This class defines a simple interpolating proof system.
This class defines a simple interpolating proof system.
Author:
Author:
Ken McMillan (kenmcmil)
Ken McMillan (kenmcmil)
Revision History:
Revision History:
--*/
--*/
#ifndef IZ3PROOF_H
#define IZ3PROOF_H
@ -40,233 +40,233 @@ Revision History:
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;
/** 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};
/** Enumeration of proof rules. */
enum rule {Resolution,Assumption,Hypothesis,Theory,Axiom,Contra,Lemma,Reflexivity,Symmetry,Transitivity,Congruence,EqContra};
/** Interface to prover. */
typedef iz3base prover;
/** Interface to prover. */
typedef iz3base prover;
/** Ast type. */
typedef prover::ast ast;
/** Ast type. */
typedef prover::ast ast;
/** Object thrown in case of a proof error. */
struct proof_error {};
/** Object thrown in case of a proof error. */
struct proof_error {};
/* Null proof node */
static const node null = -1;
/* 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 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 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 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 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 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. */
/** 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);
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 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 */
/** Make a Reflexivity node. This rule produces |- x = x */
node make_reflexivity(ast con);
node make_reflexivity(ast con);
/** Make a Symmetry node. This takes a derivation of |- x = y and
produces | y = x */
/** Make a Symmetry node. This takes a derivation of |- x = y and
produces | y = x */
node make_symmetry(ast con, node prem);
node make_symmetry(ast con, node prem);
/** Make a transitivity node. This takes derivations of |- x = y
and |- y = z produces | x = z */
/** 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);
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) */
/** 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);
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. */
/** Make an equality contradicition node. This takes |- x = y
and |- !(x = y) and produces false. */
node make_eqcontra(node prem1, node prem2);
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 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 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 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 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 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 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 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 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;
}
/** 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. */
/** 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;
}
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);
/** Copy a proof node from src */
node copy(iz3proof &src, node n);
/** Resolve two lemmas on a given literal. */
/** Resolve two lemmas on a given literal. */
node resolve_lemmas(ast pivot, node left, node right);
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);
}
/** 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
/** 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
, Z3_ast assump = (Z3_ast)0, std::vector<int> *parents = 0
#endif
);
);
/** print proof node to a stream */
/** print proof node to a stream */
void print(std::ostream &s, node n);
void print(std::ostream &s, node n);
/** show proof node on stdout */
void show(node n);
/** show proof node on stdout */
void show(node n);
/** Construct a proof, with a given prover. */
iz3proof(prover *p){
pv = p;
}
/** Construct a proof, with a given prover. */
iz3proof(prover *p){
pv = p;
}
/** Default constructor */
iz3proof(){pv = 0;}
/** Default constructor */
iz3proof(){pv = 0;}
protected:
struct node_struct {
rule rl;
ast aux;
int frame;
std::vector<ast> conclusion;
std::vector<node> premises;
};
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;
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;
node make_node(){
nodes.push_back(node_struct());
return nodes.size()-1;
}
return n.conclusion;
}
prover::range rng;
bool weak;
stl_ext::hash_set<ast> b_lits;
ast my_or(ast x, ast y);
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;
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);
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

5446
src/interp/iz3proof_itp.cpp
View file

File diff suppressed because it is too large Load diff

148
src/interp/iz3proof_itp.h
View file

@ -1,21 +1,21 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Copyright (c) 2011 Microsoft Corporation
Module Name:
Module Name:
iz3proof.h
iz3proof.h
Abstract:
Abstract:
This class defines a simple interpolating proof system.
This class defines a simple interpolating proof system.
Author:
Author:
Ken McMillan (kenmcmil)
Ken McMillan (kenmcmil)
Revision History:
Revision History:
--*/
--*/
#ifndef IZ3PROOF_ITP_H
#define IZ3PROOF_ITP_H
@ -32,110 +32,110 @@ Revision History:
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};
/** Enumeration of proof rules. */
enum rule {Resolution,Assumption,Hypothesis,Theory,Axiom,Contra,Lemma,Reflexivity,Symmetry,Transitivity,Congruence,EqContra};
/** Interface to prover. */
typedef iz3base prover;
/** Interface to prover. */
typedef iz3base prover;
/** Ast type. */
typedef prover::ast ast;
/** Ast type. */
typedef prover::ast ast;
/** The type of proof nodes (just interpolants). */
typedef ast node;
/** The type of proof nodes (just interpolants). */
typedef ast node;
/** Object thrown in case of a proof error. */
struct proof_error {};
/** Object thrown in case of a proof error. */
struct 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 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 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 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. */
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 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. */
/** 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;
virtual node make_contra(node prem, const std::vector<ast> &conclusion) = 0;
/** Make a Reflexivity node. This rule produces |- x = x */
/** Make a Reflexivity node. This rule produces |- x = x */
virtual node make_reflexivity(ast con) = 0;
virtual node make_reflexivity(ast con) = 0;
/** Make a Symmetry node. This takes a derivation of |- x = y and
produces | y = x */
/** 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;
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 */
/** 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;
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,...) */
/** 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;
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...) */
/** 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;
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 */
/** 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;
virtual node make_mp(const ast &x_eq_y, const ast &prem1, const ast &prem2) = 0;
/** Make a farkas proof node. */
/** 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;
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, 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 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;
/* 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;
/* 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);
/** 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)
{
}
iz3proof_itp(iz3mgr &m)
: iz3mgr(m)
{
}
public:
virtual ~iz3proof_itp(){
}
virtual ~iz3proof_itp(){
}
};
#endif

406
src/interp/iz3scopes.cpp
View file

@ -1,21 +1,21 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Copyright (c) 2011 Microsoft Corporation
Module Name:
Module Name:
iz3scopes.cpp
iz3scopes.cpp
Abstract:
Abstract:
Calculations with scopes, for both sequence and tree interpolation.
Calculations with scopes, for both sequence and tree interpolation.
Author:
Author:
Ken McMillan (kenmcmil)
Ken McMillan (kenmcmil)
Revision History:
Revision History:
--*/
--*/
#include <assert.h>
@ -26,294 +26,294 @@ Revision History:
/** 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(!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;
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;
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;
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;
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;
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;
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;
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;
range res;
res.lo = tree_lca(rng1.lo,rng2.lo);
res.hi = tree_gcd(rng1.hi,rng2.hi);
return res;
}
#else
namespace std {
namespace std {
template <>
class hash<scopes::range_lo > {
public:
size_t operator()(const scopes::range_lo &p) const {
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);
}
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 {
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;
}
};
}
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;
}
};
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 {
namespace std {
template <>
class hash<range_op > {
public:
size_t operator()(const range_op &p) const {
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);
}
template <> inline
size_t stdext::hash_value<range_op >(const range_op& p)
{
std::hash<range_op> h;
return h(p);
}
namespace std {
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);
}
};
}
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;
};
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::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){
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;
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;}
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;
}
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;
}
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){
/** 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();
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;
/** 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;
if(!lo) hi = SHRT_MIN;
return range(hi,lo);
}
}
/** is this range empty? */
bool scopes::range_is_empty(const range &rng){
/** 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 an empty range */
scopes::range scopes::range_empty(){
return range(SHRT_MIN,0);
}
}
/** return a full range */
scopes::range scopes::range_full(){
/** 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 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 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){
/** 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]];
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;
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);
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){
/** 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){
/** 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);
}
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 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);
}
/** 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;
}
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

292
src/interp/iz3scopes.h
View file

@ -1,21 +1,21 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Copyright (c) 2011 Microsoft Corporation
Module Name:
Module Name:
iz3scopes.h
iz3scopes.h
Abstract:
Abstract:
Calculations with scopes, for both sequence and tree interpolation.
Calculations with scopes, for both sequence and tree interpolation.
Author:
Author:
Ken McMillan (kenmcmil)
Ken McMillan (kenmcmil)
Revision History:
Revision History:
--*/
--*/
#ifndef IZ3SOPES_H
@ -28,174 +28,174 @@ Revision History:
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;
/** Construct from parents vector. */
scopes(const std::vector<int> &_parents){
parents = _parents;
}
short lo, hi;
};
/** computes the lub (smallest containing subtree) of two ranges */
range range_lub(const range &rng1, const range &rng2);
scopes(){
}
/** computes the glb (intersection) of two ranges */
range range_glb(const range &rng1, const range &rng2);
void initialize(const std::vector<int> &_parents){
parents = _parents;
}
/** is this range empty? */
bool range_is_empty(const range &rng){
return rng.hi < rng.lo;
}
/** The parents vector defining the tree structure */
std::vector<int> parents;
/** is this range full? */
bool range_is_full(const range &rng){
return rng.lo == SHRT_MIN && rng.hi == SHRT_MAX;
}
// #define FULL_TREE
#ifndef FULL_TREE
struct range {
range(){
lo = SHRT_MAX;
hi = SHRT_MIN;
}
short lo, hi;
};
/** return an empty range */
range range_empty(){
range res;
res.lo = SHRT_MAX;
res.hi = SHRT_MIN;
return res;
}
/** 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);
/** return an empty range */
range range_full(){
range res;
res.lo = SHRT_MIN;
res.hi = SHRT_MAX;
return res;
}
/** is this range empty? */
bool range_is_empty(const range &rng){
return rng.hi < rng.lo;
}
/** return the maximal element of a range */
int range_max(const range &rng){
return rng.hi;
}
/** is this range full? */
bool range_is_full(const range &rng){
return rng.lo == SHRT_MIN && rng.hi == SHRT_MAX;
}
/** return a minimal (not necessarily unique) element of a range */
int range_min(const range &rng){
return rng.lo;
}
/** return an empty range */
range range_empty(){
range res;
res.lo = SHRT_MAX;
res.hi = SHRT_MIN;
return res;
}
/** 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;
}
/** return an empty range */
range range_full(){
range res;
res.lo = SHRT_MIN;
res.hi = SHRT_MAX;
return res;
}
void range_add(int i, range &n){
/** 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;
if(i > n.hi) n.hi = i;
#else
range rng; rng.lo = i; rng.hi = i;
n = range_lub(rng,n);
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);
/** 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_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;
}
};
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;
range_tables *rt;
/** computes the lub (smallest containing subtree) of two ranges */
range range_lub(const range &rng1, const range &rng2);
/** 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);
/** 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);
/** is this range empty? */
bool range_is_empty(const range &rng);
/** return an empty range */
range range_empty();
/** return an empty range */
range range_empty();
/** return a full range */
range range_full();
/** return a full range */
range range_full();
/** return the maximal element of a range */
int range_max(const range &rng);
/** 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 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);
/** 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);
/** 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);
/** 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);
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 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 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);
/** 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;}
int tree_lca(int n1, int n2);
int tree_gcd(int n1, int n2);
bool tree_mode(){return parents.size() != 0;}
@ -205,17 +205,17 @@ class scopes {
#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;
}
};
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;
return x.lo == y.lo && x.hi == y.hi;
}
#endif

24
src/interp/iz3secondary.h
View file

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

3684
src/interp/iz3translate.cpp
View file

File diff suppressed because it is too large Load diff

46
src/interp/iz3translate.h
View file

@ -1,22 +1,22 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Copyright (c) 2011 Microsoft Corporation
Module Name:
Module Name:
iz3translate.h
iz3translate.h
Abstract:
Abstract:
Interface for proof translations from Z3 proofs to interpolatable
proofs.
Interface for proof translations from Z3 proofs to interpolatable
proofs.
Author:
Author:
Ken McMillan (kenmcmil)
Ken McMillan (kenmcmil)
Revision History:
Revision History:
--*/
--*/
#ifndef IZ3TRANSLATION_H
@ -29,27 +29,27 @@ Revision History:
// 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(){}
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 {
};
/** This is thrown when the proof cannot be translated. */
struct unsupported {
};
static iz3translation *create(iz3mgr &mgr,
iz3secondary *secondary,
const std::vector<std::vector<ast> > &frames,
const std::vector<int> &parents,
const std::vector<ast> &theory);
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) {}
: iz3base(mgr,_cnsts,_parents,_theory) {}
};
//#define IZ3_TRANSLATE_DIRECT2

2986
src/interp/iz3translate_direct.cpp
View file

File diff suppressed because it is too large Load diff

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

File diff suppressed because it is too large Load diff

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

@ -1,22 +1,22 @@
/*++
Copyright (c) 2013 Microsoft Corporation
Copyright (c) 2013 Microsoft Corporation
Module Name:
Module Name:
duality_dl_interface.h
duality_dl_interface.h
Abstract:
Abstract:
SMT2 interface for Duality
SMT2 interface for Duality
Author:
Author:
Krystof Hoder (t-khoder) 2011-9-22.
Modified by Ken McMIllan (kenmcmil) 2013-4-18.
Krystof Hoder (t-khoder) 2011-9-22.
Modified by Ken McMIllan (kenmcmil) 2013-4-18.
Revision History:
Revision History:
--*/
--*/
#ifndef _DUALITY_DL_INTERFACE_H_
#define _DUALITY_DL_INTERFACE_H_