mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

debugging interpolation

Browse source
This commit is contained in:
Ken McMillan 2013-03-06 18:26:46 -08:00
parent ae9276ad9b
commit 2b93537366
10 changed files with 121 additions and 47 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

22
scripts/mk_util.py
View file

@ -71,6 +71,7 @@ VER_BUILD=None
VER_REVISION=None
PREFIX=os.path.split(os.path.split(os.path.split(PYTHON_PACKAGE_DIR)[0])[0])[0]
GMP=False
FOCI2=False
VS_PAR=False
VS_PAR_NUM=8
GPROF=False
@ -199,6 +200,14 @@ def test_gmp(cc):
t.commit()
return exec_compiler_cmd([cc, CPPFLAGS, 'tstgmp.cpp', LDFLAGS, '-lgmp']) == 0
def test_foci2(cc):
if is_verbose():
print("Testing FOCI2...")
t = TempFile('tstfoci2.cpp')
t.add('#include<foci2.h>\nint main() { mpz_t t; mpz_init(t); mpz_clear(t); return 0; }\n')
t.commit()
return exec_compiler_cmd([cc, CPPFLAGS, 'tstfoci2.cpp', LDFLAGS, '-lfoci2']) == 0
def test_openmp(cc):
if is_verbose():
print("Testing OpenMP...")
@ -444,6 +453,7 @@ def display_help(exit_code):
if not IS_WINDOWS:
print(" -g, --gmp use GMP.")
print(" --gprof enable gprof")
print(" --foci2 use FOCI2.")
print("")
print("Some influential environment variables:")
if not IS_WINDOWS:
@ -459,7 +469,7 @@ def display_help(exit_code):
# Parse configuration option for mk_make script
def parse_options():
global VERBOSE, DEBUG_MODE, IS_WINDOWS, VS_X64, ONLY_MAKEFILES, SHOW_CPPS, VS_PROJ, TRACE, VS_PAR, VS_PAR_NUM
global DOTNET_ENABLED, JAVA_ENABLED, STATIC_LIB, PREFIX, GMP, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH
global DOTNET_ENABLED, JAVA_ENABLED, STATIC_LIB, PREFIX, GMP, FOCI2, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH
try:
options, remainder = getopt.gnu_getopt(sys.argv[1:],
'b:dsxhmcvtnp:gj',
@ -508,6 +518,8 @@ def parse_options():
VS_PAR_NUM = int(arg)
elif opt in ('-g', '--gmp'):
GMP = True
elif opt in ('-f', '--foci2'):
FOCI2 = True
elif opt in ('-j', '--java'):
JAVA_ENABLED = True
elif opt == '--gprof':
@ -1458,7 +1470,7 @@ def mk_config():
print('JNI Bindings: %s' % JNI_HOME)
print('Java Compiler: %s' % JAVAC)
else:
global CXX, CC, GMP, CPPFLAGS, CXXFLAGS, LDFLAGS
global CXX, CC, GMP, FOCI2, CPPFLAGS, CXXFLAGS, LDFLAGS
ARITH = "internal"
check_ar()
CXX = find_cxx_compiler()
@ -1475,6 +1487,12 @@ def mk_config():
SLIBEXTRAFLAGS = '%s -lgmp' % SLIBEXTRAFLAGS
else:
CPPFLAGS = '%s -D_MP_INTERNAL' % CPPFLAGS
if FOCI2:
test_foci2(CXX)
LDFLAGS = '%s -lfoci2' % LDFLAGS
SLIBEXTRAFLAGS = '%s -lfoci2' % SLIBEXTRAFLAGS
else:
CPPFLAGS = '%s -D_MP_INTERNAL' % CPPFLAGS
if GIT_HASH:
CPPFLAGS = '%s -DZ3GITHASH=%s' % (CPPFLAGS, GIT_HASH)
CXXFLAGS = '%s -c' % CXXFLAGS

21
src/api/api_interp.cpp
View file

@ -90,7 +90,7 @@ extern "C" {
ptr_vector<ast> interpolants(num-1); // make space for result
scoped_ptr<ast_manager> _m(&mk_c(ctx)->m());
ast_manager &_m = mk_c(ctx)->m();
iz3interpolate(_m,
to_ast(proof),
pre_cnsts_vec,
@ -100,10 +100,12 @@ extern "C" {
0); // ignore params for now FIXME
// copy result back
for(unsigned i = 0; i < interpolants.size(); i++)
for(unsigned i = 0; i < interpolants.size(); i++){
mk_c(ctx)->save_ast_trail(interpolants[i]);
interps[i] = of_ast(interpolants[i]);
_m.dec_ref(interpolants[i]);
}
}
}
Z3_lbool Z3_interpolate(Z3_context ctx,
@ -120,6 +122,8 @@ extern "C" {
){
profiling::timer_start("Solve");
if(!incremental){
profiling::timer_start("Z3 assert");
@ -159,6 +163,10 @@ extern "C" {
interps,
num_theory,
theory);
if(!incremental)
for(int i = 0; i < num-1; i++)
Z3_persist_ast(ctx,interps[i],1);
break;
case Z3_L_UNDEF:
@ -172,6 +180,13 @@ extern "C" {
break;
}
profiling::timer_start("Z3 pop");
if(!incremental)
Z3_pop(ctx,1);
profiling::timer_stop("Z3 pop");
profiling::timer_stop("Solve");
return result;
}

4
src/interp/iz3base.cpp
View file

@ -140,7 +140,7 @@ iz3base::ast iz3base::simplify_with_lit_rec(ast n, ast lit, stl_ext::hash_map<as
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)0);
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;
@ -159,7 +159,7 @@ iz3base::ast iz3base::simplify_with_lit(ast n, ast lit){
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)0);
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;

2
src/interp/iz3base.h
View file

@ -56,7 +56,7 @@ class iz3base : public iz3mgr, public scopes {
/** Constructor */
iz3base(scoped_ptr<ast_manager> &_m_manager,
iz3base(ast_manager &_m_manager,
const std::vector<ast> &_cnsts,
const std::vector<int> &_parents,
const std::vector<ast> &_theory)

2
src/interp/iz3foci.cpp
View file

@ -197,7 +197,7 @@ public:
// convert an expr to Z3 ast
ast to_Z3_ast(foci2::ast i){
std::pair<foci2::ast,ast> foo(i,(ast)0);
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;

20
src/interp/iz3interp.cpp
View file

@ -224,11 +224,11 @@ public:
delete sp;
}
iz3interp(scoped_ptr<ast_manager> &_m_manager)
iz3interp(ast_manager &_m_manager)
: iz3mgr(_m_manager) {}
};
void iz3interpolate(scoped_ptr<ast_manager> &_m_manager,
void iz3interpolate(ast_manager &_m_manager,
ast *proof,
const ptr_vector<ast> &cnsts,
const ::vector<int> &parents,
@ -236,21 +236,21 @@ void iz3interpolate(scoped_ptr<ast_manager> &_m_manager,
const ptr_vector<ast> &theory,
interpolation_options_struct * options)
{
std::vector<ast_r> _cnsts(cnsts.size());
iz3interp itp(_m_manager);
std::vector<iz3mgr::ast> _cnsts(cnsts.size());
std::vector<int> _parents(parents.size());
std::vector<ast_r> _interps;
std::vector<ast_r> _theory(theory.size());
std::vector<iz3mgr::ast> _interps;
std::vector<iz3mgr::ast> _theory(theory.size());
for(unsigned i = 0; i < cnsts.size(); i++)
_cnsts[i] = cnsts[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] = theory[i];
ast_r _proof(proof);
iz3interp itp(_m_manager);
_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] = interps[i];
interps[i] = itp.uncook(_interps[i]);
}

2
src/interp/iz3interp.h
View file

@ -29,7 +29,7 @@ struct interpolation_options_struct {
typedef interpolation_options_struct *interpolation_options;
void iz3interpolate(scoped_ptr<ast_manager> &_m_manager,
void iz3interpolate(ast_manager &_m_manager,
ast *proof,
const ptr_vector<ast> &cnsts,
const ::vector<int> &parents,

14
src/interp/iz3mgr.cpp
View file

@ -40,7 +40,7 @@ std::ostream &operator <<(std::ostream &s, const iz3mgr::ast &a){
iz3mgr::ast iz3mgr::make_var(const std::string &name, type ty){
symbol s = symbol(name.c_str());
return m().mk_const(m().mk_const_decl(s, ty));
return cook(m().mk_const(m().mk_const_decl(s, ty)));
}
iz3mgr::ast iz3mgr::make(opr op, int n, raw_ast **args){
@ -91,7 +91,7 @@ iz3mgr::ast iz3mgr::make(opr op, int n, raw_ast **args){
}
iz3mgr::ast iz3mgr::mki(family_id fid, decl_kind dk, int n, raw_ast **args){
return m().mk_app(fid, dk, 0, 0, n, (expr **)args);
return cook(m().mk_app(fid, dk, 0, 0, n, (expr **)args));
}
iz3mgr::ast iz3mgr::make(opr op, const std::vector<ast> &args){
@ -128,7 +128,7 @@ iz3mgr::ast iz3mgr::make(opr op, ast &arg0, ast &arg1, ast &arg2){
}
iz3mgr::ast iz3mgr::make(symb sym, int n, raw_ast **args){
return m().mk_app(sym, n, (expr **) args);
return cook(m().mk_app(sym, n, (expr **) args));
}
iz3mgr::ast iz3mgr::make(symb sym, const std::vector<ast> &args){
@ -193,14 +193,16 @@ iz3mgr::ast iz3mgr::make_quant(opr op, const std::vector<ast> &bvs, ast &body){
0, 0,
0, 0
);
return result.get();
return cook(result.get());
}
// FIXME replace this with existing Z3 functionality
iz3mgr::ast iz3mgr::clone(ast &t, const std::vector<ast> &_args){
if(_args.size() == 0)
return t;
ast_manager& m = *m_manager.get();
ast_manager& m = m_manager;
expr* a = to_expr(t.raw());
static std::vector<raw_ast*> rargs(10);
if(rargs.size() < _args.size())
@ -231,7 +233,7 @@ iz3mgr::ast iz3mgr::clone(ast &t, const std::vector<ast> &_args){
default:
break;
}
return a;
return cook(a);
}

75
src/interp/iz3mgr.h
View file

@ -53,32 +53,65 @@ Revision History:
typedef ast raw_ast;
/** Wrapper around an ast pointer */
class ast_r {
class ast_i {
protected:
raw_ast *_ast;
public:
raw_ast * const &raw() const {return _ast;}
ast_r(raw_ast *a){_ast = a;}
ast_i(raw_ast *a){_ast = a;}
ast_r(){_ast = 0;}
bool eq(const ast_r &other) const {
ast_i(){_ast = 0;}
bool eq(const ast_i &other) const {
return _ast == other._ast;
}
bool lt(const ast_r &other) const {
bool lt(const ast_i &other) const {
return _ast < other._ast;
}
friend bool operator==(const ast_r &x, const ast_r&y){
friend bool operator==(const ast_i &x, const ast_i&y){
return x.eq(y);
}
friend bool operator!=(const ast_r &x, const ast_r&y){
friend bool operator!=(const ast_i &x, const ast_i&y){
return !x.eq(y);
}
friend bool operator<(const ast_r &x, const ast_r&y){
friend bool operator<(const ast_i &x, const ast_i&y){
return x.lt(y);
}
size_t hash() const {return (size_t)_ast;}
bool null() const {return !_ast;}
};
/** Reference counting verison of above */
class ast_r : public ast_i {
ast_manager *_m;
public:
ast_r(ast_manager *m, raw_ast *a) : ast_i(a) {
_m = m;
m->inc_ref(a);
}
ast_r() {_m = 0;}
ast_r(const ast_r &other) : ast_i(other) {
_m = other._m;
_m->inc_ref(_ast);
}
ast_r &operator=(const ast_r &other) {
if(_ast)
_m->dec_ref(_ast);
_ast = other._ast;
_m = other._m;
_m->inc_ref(_ast);
return *this;
}
~ast_r(){
if(_ast)
_m->dec_ref(_ast);
}
};
// to make ast_r hashable
namespace stl_ext {
@ -186,8 +219,14 @@ class iz3mgr {
ast make_quant(opr op, const std::vector<ast> &bvs, ast &body);
ast clone(ast &t, const std::vector<ast> &args);
ast_manager &m() {return *m_manager.get();}
ast_manager &m() {return m_manager;}
ast cook(raw_ast *a) {return ast(&m_manager,a);}
raw_ast *uncook(const ast &a) {
m_manager.inc_ref(a.raw());
return a.raw();
}
/** Methods for destructing ast. */
@ -210,13 +249,13 @@ class iz3mgr {
ast_kind dk = t.raw()->get_kind();
switch(dk){
case AST_APP:
return to_app(t.raw())->get_arg(i);
return cook(to_app(t.raw())->get_arg(i));
case AST_QUANTIFIER:
return to_quantifier(t.raw())->get_expr();
return cook(to_quantifier(t.raw())->get_expr());
default:;
}
assert(0);
return ast((raw_ast *)0);
return ast();
}
symb sym(ast t){
@ -262,7 +301,7 @@ class iz3mgr {
}
ast get_quantifier_body(const ast &t) {
return to_quantifier(t.raw())->get_expr();
return cook(to_quantifier(t.raw())->get_expr());
}
unsigned get_variable_index_value(const ast &t) {
@ -359,7 +398,7 @@ class iz3mgr {
ast make_int(const std::string &s) {
sort *r = m().mk_sort(m_arith_fid, INT_SORT);
return m_arith_util.mk_numeral(rational(s.c_str()),r);
return cook(m_arith_util.mk_numeral(rational(s.c_str()),r));
}
@ -392,9 +431,9 @@ class iz3mgr {
static void pretty_print(std::ostream &f, const std::string &s);
iz3mgr(scoped_ptr<ast_manager> &_m_manager)
iz3mgr(ast_manager &_m_manager)
: m_manager(_m_manager),
m_arith_util(*_m_manager)
m_arith_util(_m_manager)
{
m_basic_fid = m().get_basic_family_id();
m_arith_fid = m().mk_family_id("arith");
@ -406,7 +445,7 @@ class iz3mgr {
iz3mgr(const iz3mgr& other)
: m_manager(other.m_manager),
m_arith_util((const arith_util&)*other.m_manager)
m_arith_util(other.m_manager)
{
m_basic_fid = m().get_basic_family_id();
m_arith_fid = m().mk_family_id("arith");
@ -417,7 +456,7 @@ class iz3mgr {
}
protected:
scoped_ptr<ast_manager> m_manager;
ast_manager &m_manager;
private:
ast mki(family_id fid, decl_kind sk, int n, raw_ast **args);

6
src/interp/iz3translate_direct.cpp
View file

@ -625,7 +625,7 @@ public:
ast cont_eq(bool truth, ast v, ast e){
if(is_not(e)) return cont_eq(!truth,v,arg(e,0));
if(cont_eq_memo.find(e) != cont_eq_memo.end())
return (ast)0;
return ast();
cont_eq_memo.insert(e);
if(!truth && op(e) == Equal){
if(arg(e,0) == v) return(arg(e,1));
@ -645,7 +645,7 @@ public:
ast subst(ast var, ast t, ast e){
if(e == var) return t;
std::pair<ast,ast> foo(e,(ast)0);
std::pair<ast,ast> foo(e,ast());
std::pair<AstToAst::iterator,bool> bar = subst_memo.insert(foo);
ast &res = bar.first->second;
if(bar.second){
@ -1722,7 +1722,7 @@ public:
for(unsigned i = 0; i < theory.size(); i++)
frame_map[theory[i]] = INT_MAX;
frames = cnsts.size();
traced_lit = 0;
traced_lit = ast();
}
};