mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

tabs

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-05-19 11:01:15 +01:00
parent 25f37c8a0c
commit 32fb679066
17 changed files with 141 additions and 142 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/api/api_context.cpp
View file

@ -89,7 +89,7 @@ namespace api {
m_bv_util(m()),
m_datalog_util(m()),
m_fpa_util(m()),
m_dtutil(m()),
m_dtutil(m()),
m_last_result(m()),
m_ast_trail(m()),
m_replay_stack() {

2
src/ast/simplifier/inj_axiom.cpp
View file

@ -114,7 +114,7 @@ bool simplify_inj_axiom(ast_manager & m, quantifier * q, expr_ref & result) {
ptr_vector<sort> domain;
inv_vars.push_back(f);
for (unsigned i = 0; i < inv_vars.size(); ++i) {
for (unsigned i = 0; i < inv_vars.size(); ++i) {
domain.push_back(m.get_sort(inv_vars[i]));
}
sort * d = decl->get_domain(idx);

10
src/cmd_context/interpolant_cmds.cpp
View file

@ -36,11 +36,11 @@
#include"scoped_proof.h"
static void show_interpolant_and_maybe_check(cmd_context & ctx,
ptr_vector<ast> &cnsts,
expr *t,
ptr_vector<ast> &interps,
params_ref &m_params,
bool check)
ptr_vector<ast> &cnsts,
expr *t,
ptr_vector<ast> &interps,
params_ref &m_params,
bool check)
{
if (m_params.get_bool("som", false))

16
src/duality/duality_rpfp.cpp
View file

@ -1171,7 +1171,7 @@ namespace Duality {
new_alits.push_back(conj);
#endif
slvr().add(ctx.make(Implies, res, conj));
// std::cout << res << ": " << conj << "\n";
// std::cout << res << ": " << conj << "\n";
}
if (opt_map)
(*opt_map)[res] = conj;
@ -2734,7 +2734,7 @@ namespace Duality {
if(res != unsat)
throw "should be unsat";
s.pop(1);
for(unsigned i = 0; i < conjuncts.size(); ){
std::swap(conjuncts[i],conjuncts.back());
expr save = conjuncts.back();
@ -3056,7 +3056,7 @@ namespace Duality {
Push();
expr the_impl = is.get_implicant();
if(eq(the_impl,prev_impl)){
// std::cout << "got old implicant\n";
// std::cout << "got old implicant\n";
repeated_case_count++;
}
prev_impl = the_impl;
@ -3126,8 +3126,8 @@ namespace Duality {
axioms_added = true;
}
else {
//#define KILL_ON_BAD_INTERPOLANT
#ifdef KILL_ON_BAD_INTERPOLANT
//#define KILL_ON_BAD_INTERPOLANT
#ifdef KILL_ON_BAD_INTERPOLANT
std::cout << "bad in InterpolateByCase -- core:\n";
#if 0
std::vector<expr> assumps;
@ -3137,7 +3137,7 @@ namespace Duality {
#endif
std::cout << "checking for inconsistency\n";
std::cout << "model:\n";
is.get_model().show();
is.get_model().show();
expr impl = is.get_implicant();
std::vector<expr> conjuncts;
CollectConjuncts(impl,conjuncts,true);
@ -3379,7 +3379,7 @@ namespace Duality {
int arity = f.arity();
std::vector<sort> domain;
for(int i = 0; i < arity; i++)
domain.push_back(f.domain(i));
domain.push_back(f.domain(i));
return ctx.function(name.c_str(), arity, &domain[0], f.range());
}
@ -3390,7 +3390,7 @@ namespace Duality {
int arity = f.arity();
std::vector<sort> domain;
for(int i = 0; i < arity; i++)
domain.push_back(f.domain(i));
domain.push_back(f.domain(i));
return ctx.function(name.c_str(), arity, &domain[0], f.range());
}

37
src/duality/duality_solver.cpp
View file

@ -55,7 +55,7 @@
// #define KEEP_EXPANSIONS
// #define USE_CACHING_RPFP
// #define PROPAGATE_BEFORE_CHECK
#define NEW_STRATIFIED_INLINING
#define NEW_STRATIFIED_INLINING
#define USE_RPFP_CLONE
#define USE_NEW_GEN_CANDS
@ -389,7 +389,7 @@ namespace Duality {
else InstantiateAllEdges();
}
else {
#ifdef NEW_STRATIFIED_INLINING
#ifdef NEW_STRATIFIED_INLINING
#else
CreateLeaves();
@ -929,7 +929,7 @@ namespace Duality {
int StratifiedLeafCount;
#ifdef NEW_STRATIFIED_INLINING
#ifdef NEW_STRATIFIED_INLINING
/** Stratified inlining builds an initial layered unwinding before
switching to the LAWI strategy. Currently the number of layers
@ -1135,7 +1135,6 @@ namespace Duality {
conj = rpfp->conjoin(conjs);
}
}
Node *CreateUnderapproxNode(Node *node){
// cex.get_tree()->ComputeUnderapprox(cex.get_root(),0);
@ -1872,7 +1871,7 @@ namespace Duality {
underapproximations as upper bounds. This mode is used to
complete the partial derivation constructed in underapprox
mode.
*/
*/
bool Derive(RPFP *rpfp, RPFP::Node *root, bool _underapprox, bool _constrained = false, RPFP *_tree = 0){
underapprox = _underapprox;
@ -2066,7 +2065,7 @@ namespace Duality {
if(!top->Outgoing || tree->Check(top,unused_set) == unsat){
unused_set.resize(orig_unused);
if(to - from == 1){
#if 1
#if 1
std::cout << "Not using underapprox of " << used_set[from] ->number << std::endl;
#endif
choices.insert(used_set[from]);
@ -2250,14 +2249,14 @@ namespace Duality {
throw "stacks out of sync!";
reporter->Depth(stack.size());
// res = tree->Solve(top, 1); // incremental solve, keep interpolants for one pop
// res = tree->Solve(top, 1); // incremental solve, keep interpolants for one pop
check_result foo = Check();
res = foo == unsat ? l_false : l_true;
if (res == l_false) {
if (stack.empty()) // should never happen
return false;
{
std::vector<Node *> &expansions = stack.back().expansions;
int update_count = 0;
@ -2384,7 +2383,7 @@ namespace Duality {
tree->Pop(1);
node_order.clear();
while(stack.size() > 1){
tree->Pop(1);
tree->Pop(1);
std::vector<Node *> &expansions = stack.back().expansions;
for(unsigned i = 0; i < expansions.size(); i++)
node_order.push_back(expansions[i]);
@ -2420,12 +2419,12 @@ namespace Duality {
void PopLevel(){
std::vector<Node *> &expansions = stack.back().expansions;
tree->Pop(1);
tree->Pop(1);
hash_set<Node *> leaves_to_remove;
for(unsigned i = 0; i < expansions.size(); i++){
Node *node = expansions[i];
// if(node != top)
// tree->ConstrainParent(node->Incoming[0],node);
// if(node != top)
//tree->ConstrainParent(node->Incoming[0],node);
std::vector<Node *> &cs = node->Outgoing->Children;
for(unsigned i = 0; i < cs.size(); i++){
leaves_to_remove.insert(cs[i]);
@ -2441,7 +2440,7 @@ namespace Duality {
}
stack.pop_back();
}
bool NodeTooComplicated(Node *node){
int ops = tree->CountOperators(node->Annotation.Formula);
if(ops > 10) return true;
@ -2670,7 +2669,7 @@ namespace Duality {
}
}
}
#endif
#endif
}
@ -2732,7 +2731,7 @@ namespace Duality {
return false;
if(parent->underapprox_map.find(covering) != parent->underapprox_map.end())
return covering->number < covered->number || parent->underapprox_map[covering] == covered;
#endif
#endif
return covering->number < covered->number;
}
@ -2778,7 +2777,7 @@ namespace Duality {
else
return false;
}
#endif
#endif
bool Close(Node *node){
if(covered_by(node))
@ -2842,7 +2841,7 @@ namespace Duality {
#ifdef UNDERAPPROX_NODES
// if(parent->underapprox_map.find(covering) != parent->underapprox_map.end())
// return parent->underapprox_map[covering] == covered;
#endif
#endif
if(CoverOrder(covering,covered)
&& !IsCovered(covering)){
RPFP::Transformer f(covering->Annotation); f.SetEmpty();
@ -3175,7 +3174,7 @@ namespace Duality {
// else
// std::cout << "constant not matched\n";
}
RPFP *old_unwinding = old_solver->unwinding;
hash_map<std::string, std::vector<Node *> > pred_match;
@ -3467,7 +3466,7 @@ namespace Duality {
dnode->Bound.Formula = bound_fmla;
}
db_saved_bounds.push_back(bound_fmla);
// dnode->Annotation.Formula = ctx.make(And,node->Annotation.Formula,ctx.make(Geq,dvar,ctx.int_val(0)));
// dnode->Annotation.Formula = ctx.make(And,node->Annotation.Formula,ctx.make(Geq,dvar,ctx.int_val(0)));
}
for(unsigned i = 0; i < rpfp->edges.size(); i++){
Edge *edge = rpfp->edges[i];

2
src/duality/duality_wrapper.cpp
View file

@ -727,7 +727,7 @@ namespace Duality {
if(!started){
sw.start();
started = true;
}
}
return sw.get_current_seconds();
}

30
src/interp/iz3base.cpp
View file

@ -292,14 +292,14 @@ bool iz3base::is_sat(const std::vector<ast> &q, ast &_proof, std::vector<ast> &v
void iz3base::find_children(const stl_ext::hash_set<ast> &cnsts_set,
const ast &tree,
std::vector<ast> &cnsts,
std::vector<int> &parents,
std::vector<ast> &conjuncts,
std::vector<int> &children,
std::vector<int> &pos_map,
bool merge
){
const ast &tree,
std::vector<ast> &cnsts,
std::vector<int> &parents,
std::vector<ast> &conjuncts,
std::vector<int> &children,
std::vector<int> &pos_map,
bool merge
){
std::vector<int> my_children;
std::vector<ast> my_conjuncts;
if(op(tree) == Interp){ // if we've hit an interpolation position...
@ -336,13 +336,13 @@ void iz3base::find_children(const stl_ext::hash_set<ast> &cnsts_set,
}
void iz3base::to_parents_vec_representation(const std::vector<ast> &_cnsts,
const ast &tree,
std::vector<ast> &cnsts,
std::vector<int> &parents,
std::vector<ast> &theory,
std::vector<int> &pos_map,
bool merge
){
const ast &tree,
std::vector<ast> &cnsts,
std::vector<int> &parents,
std::vector<ast> &theory,
std::vector<int> &pos_map,
bool merge
){
std::vector<int> my_children;
std::vector<ast> my_conjuncts;
hash_set<ast> cnsts_set;

36
src/interp/iz3checker.cpp
View file

@ -144,7 +144,7 @@ struct iz3checker : iz3base {
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()));
@ -192,35 +192,35 @@ std::vector<T> to_std_vector(const ::vector<T> &v){
bool iz3check(ast_manager &_m_manager,
solver *s,
std::ostream &err,
const ptr_vector<ast> &cnsts,
const ::vector<int> &parents,
const ptr_vector<ast> &interps,
const ptr_vector<ast> &theory)
solver *s,
std::ostream &err,
const ptr_vector<ast> &cnsts,
const ::vector<int> &parents,
const ptr_vector<ast> &interps,
const ptr_vector<ast> &theory)
{
iz3checker chk(_m_manager);
return chk.check(s,err,chk.cook(cnsts),to_std_vector(parents),chk.cook(interps),chk.cook(theory));
}
bool iz3check(iz3mgr &mgr,
solver *s,
std::ostream &err,
const std::vector<iz3mgr::ast> &cnsts,
const std::vector<int> &parents,
const std::vector<iz3mgr::ast> &interps,
const std::vector<iz3mgr::ast> &theory)
solver *s,
std::ostream &err,
const std::vector<iz3mgr::ast> &cnsts,
const std::vector<int> &parents,
const std::vector<iz3mgr::ast> &interps,
const std::vector<iz3mgr::ast> &theory)
{
iz3checker chk(mgr);
return chk.check(s,err,cnsts,parents,interps,theory);
}
bool iz3check(ast_manager &_m_manager,
solver *s,
std::ostream &err,
const ptr_vector<ast> &_cnsts,
ast *tree,
const ptr_vector<ast> &interps)
solver *s,
std::ostream &err,
const ptr_vector<ast> &_cnsts,
ast *tree,
const ptr_vector<ast> &interps)
{
iz3checker chk(_m_manager);
return chk.check(s,err,chk.cook(_cnsts),chk.cook(tree),chk.cook(interps));

48
src/interp/iz3interp.cpp
View file

@ -252,7 +252,7 @@ public:
// 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
@ -420,12 +420,12 @@ public:
void iz3interpolate(ast_manager &_m_manager,
ast *proof,
const ptr_vector<ast> &cnsts,
const ::vector<int> &parents,
ptr_vector<ast> &interps,
const ptr_vector<ast> &theory,
interpolation_options_struct * options)
ast *proof,
const ptr_vector<ast> &cnsts,
const ::vector<int> &parents,
ptr_vector<ast> &interps,
const ptr_vector<ast> &theory,
interpolation_options_struct * options)
{
iz3interp itp(_m_manager);
if(options)
@ -448,12 +448,12 @@ void iz3interpolate(ast_manager &_m_manager,
}
void iz3interpolate(ast_manager &_m_manager,
ast *proof,
const ::vector<ptr_vector<ast> > &cnsts,
const ::vector<int> &parents,
ptr_vector<ast> &interps,
const ptr_vector<ast> &theory,
interpolation_options_struct * options)
ast *proof,
const ::vector<ptr_vector<ast> > &cnsts,
const ::vector<int> &parents,
ptr_vector<ast> &interps,
const ptr_vector<ast> &theory,
interpolation_options_struct * options)
{
iz3interp itp(_m_manager);
if(options)
@ -477,11 +477,11 @@ void iz3interpolate(ast_manager &_m_manager,
}
void iz3interpolate(ast_manager &_m_manager,
ast *proof,
const ptr_vector<ast> &cnsts,
ast *tree,
ptr_vector<ast> &interps,
interpolation_options_struct * options)
ast *proof,
const ptr_vector<ast> &cnsts,
ast *tree,
ptr_vector<ast> &interps,
interpolation_options_struct * options)
{
iz3interp itp(_m_manager);
if(options)
@ -506,12 +506,12 @@ void iz3interpolate(ast_manager &_m_manager,
}
lbool iz3interpolate(ast_manager &_m_manager,
solver &s,
ast *tree,
ptr_vector<ast> &cnsts,
ptr_vector<ast> &interps,
model_ref &m,
interpolation_options_struct * options)
solver &s,
ast *tree,
ptr_vector<ast> &cnsts,
ptr_vector<ast> &interps,
model_ref &m,
interpolation_options_struct * options)
{
iz3interp itp(_m_manager);
if(options)

6
src/interp/iz3pp.cpp
View file

@ -107,9 +107,9 @@ public:
};
void iz3pp(ast_manager &m,
const ptr_vector<expr> &cnsts_vec,
expr *tree,
std::ostream& out) {
const ptr_vector<expr> &cnsts_vec,
expr *tree,
std::ostream& out) {
unsigned sz = cnsts_vec.size();
expr* const* cnsts = &cnsts_vec[0];

8
src/interp/iz3proof_itp.cpp
View file

@ -778,7 +778,7 @@ class iz3proof_itp_impl : public iz3proof_itp {
sum_cond_ineq(ineq2,make_int("1"),yleqx,Aproves2,Bproves2);
ast Bcond = my_implies(Bproves1,my_and(Aproves1,z3_simplify(ineq2)));
// if(!is_true(Aproves1) || !is_true(Bproves1))
// std::cout << "foo!\n";;
// std::cout << "foo!\n";;
if(y == make_int(rational(0)) && op(x) == Plus && num_args(x) == 2){
if(get_term_type(arg(x,0)) == LitA){
ast iter = z3_simplify(make(Plus,arg(x,0),get_ineq_rhs(xleqy)));
@ -915,7 +915,7 @@ class iz3proof_itp_impl : public iz3proof_itp {
int ipos = pos.get_unsigned();
ast cond = mk_true();
ast equa = sep_cond(arg(pf,0),cond);
#if 0
#if 0
if(op(equa) == Equal){
ast pe = mk_not(neg_equality);
ast lhs = subst_in_arg_pos(ipos,arg(equa,0),arg(pe,0));
@ -2784,7 +2784,7 @@ class iz3proof_itp_impl : public iz3proof_itp {
}
else if(o == Plus || o == Times){ // don't want bound variables inside arith ops
// std::cout << "WARNING: non-local arithmetic\n";
// frng = erng; // this term will be localized
// frng = erng; // this term will be localized
}
else if(o == Select){ // treat the array term like a function symbol
prover::range srng = pv->ast_scope(arg(e,0));
@ -2805,7 +2805,7 @@ class iz3proof_itp_impl : public iz3proof_itp {
pfs.push_back(argpf);
}
}
e = clone(e,largs);
if(pfs.size())
pf = make_congruence(eqs,make_equiv(e,orig_e),pfs);

4
src/interp/iz3scopes.cpp
View file

@ -97,7 +97,7 @@ namespace std {
template <> inline
size_t stdext::hash_value<scopes::range_lo >(const scopes::range_lo& p)
{
{
std::hash<scopes::range_lo> h;
return h(p);
}
@ -133,7 +133,7 @@ namespace std {
template <> inline
size_t stdext::hash_value<range_op >(const range_op& p)
{
{
std::hash<range_op> h;
return h(p);
}

18
src/interp/iz3translate.cpp
View file

@ -274,7 +274,7 @@ public:
ast neglit = mk_not(arg(con,i));
res.erase(neglit);
}
}
}
}
}
#if 0
@ -612,7 +612,7 @@ public:
rng = range_glb(rng,ast_scope(lit));
}
if(range_is_empty(rng)) return -1;
int hi = range_max(rng);
int hi = range_max(rng);
if(hi >= frames) return frames - 1;
return hi;
}
@ -2003,10 +2003,10 @@ public:
}
iz3translation_full(iz3mgr &mgr,
iz3secondary *_secondary,
iz3secondary *_secondary,
const std::vector<std::vector<ast> > &cnsts,
const std::vector<int> &parents,
const std::vector<ast> &theory)
const std::vector<int> &parents,
const std::vector<ast> &theory)
: iz3translation(mgr, cnsts, parents, theory)
{
frames = cnsts.size();
@ -2027,10 +2027,10 @@ public:
#ifdef IZ3_TRANSLATE_FULL
iz3translation *iz3translation::create(iz3mgr &mgr,
iz3secondary *secondary,
const std::vector<std::vector<ast> > &cnsts,
const std::vector<int> &parents,
const std::vector<ast> &theory){
iz3secondary *secondary,
const std::vector<std::vector<ast> > &cnsts,
const std::vector<int> &parents,
const std::vector<ast> &theory){
return new iz3translation_full(mgr,secondary,cnsts,parents,theory);
}

8
src/interp/iz3translate_direct.cpp
View file

@ -293,7 +293,7 @@ public:
ast neglit = mk_not(arg(con,i));
res.erase(neglit);
}
}
}
}
}
#if 0
@ -589,7 +589,7 @@ public:
rng = range_glb(rng,ast_scope(lit));
}
if(range_is_empty(rng)) return -1;
int hi = range_max(rng);
int hi = range_max(rng);
if(hi >= frames) return frames - 1;
return hi;
}
@ -881,7 +881,7 @@ public:
|| dk == PR_QUANT_INST
//|| dk == PR_UNIT_RESOLUTION
//|| dk == PR_LEMMA
)
)
return false;
if(dk == PR_HYPOTHESIS && hyps.find(con) != hyps.end())
; //std::cout << "blif!\n";
@ -1481,7 +1481,7 @@ public:
AstSet dummy;
collect_resolvent_lits(nll->proofs[i],dummy,reslits);
litset.insert(reslits.begin(),reslits.end());
}
}
}
if(to_keep.size() == nll->proofs.size()) return nll;
ResolventAppSet new_proofs;

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

@ -584,7 +584,7 @@ namespace datalog {
m_rule_properties.check_existential_tail();
m_rule_properties.check_for_negated_predicates();
break;
case DUALITY_ENGINE:
case DUALITY_ENGINE:
m_rule_properties.collect(r);
m_rule_properties.check_existential_tail();
m_rule_properties.check_for_negated_predicates();
@ -986,12 +986,12 @@ namespace datalog {
}
}
void context::get_raw_rule_formulas(expr_ref_vector& rules, svector<symbol>& names, vector<unsigned> &bounds){
void context::get_raw_rule_formulas(expr_ref_vector& rules, svector<symbol>& names, vector<unsigned> &bounds) {
for (unsigned i = 0; i < m_rule_fmls.size(); ++i) {
expr_ref r = bind_vars(m_rule_fmls[i].get(), true);
rules.push_back(r.get());
names.push_back(m_rule_names[i]);
bounds.push_back(m_rule_bounds[i]);
expr_ref r = bind_vars(m_rule_fmls[i].get(), true);
rules.push_back(r.get());
names.push_back(m_rule_names[i]);
bounds.push_back(m_rule_bounds[i]);
}
}

2
src/shell/main.cpp
View file

@ -329,7 +329,7 @@ int main(int argc, char ** argv) {
g_input_kind = IN_SMTLIB;
}
}
}
}
switch (g_input_kind) {
case IN_SMTLIB:
return_value = read_smtlib_file(g_input_file);

42
src/util/mpz.cpp
View file

@ -336,17 +336,17 @@ void mpz_manager<SYNCH>::set(mpz & target, unsigned sz, digit_t const * digits)
}
}
#else
mk_big(target);
// reset
mpz_set_ui(*target.m_ptr, digits[sz - 1]);
SASSERT(sz > 0);
unsigned i = sz - 1;
while (i > 0) {
--i;
mpz_mul_2exp(*target.m_ptr, *target.m_ptr, 32);
mpz_set_ui(m_tmp, digits[i]);
mpz_add(*target.m_ptr, *target.m_ptr, m_tmp);
}
mk_big(target);
// reset
mpz_set_ui(*target.m_ptr, digits[sz - 1]);
SASSERT(sz > 0);
unsigned i = sz - 1;
while (i > 0) {
--i;
mpz_mul_2exp(*target.m_ptr, *target.m_ptr, 32);
mpz_set_ui(m_tmp, digits[i]);
mpz_add(*target.m_ptr, *target.m_ptr, m_tmp);
}
#endif
}
}
@ -2037,16 +2037,16 @@ bool mpz_manager<SYNCH>::decompose(mpz const & a, svector<digit_t> & digits) {
}
return a.m_val < 0;
#else
bool r = is_neg(a);
mpz_set(m_tmp, *a.m_ptr);
mpz_abs(m_tmp, m_tmp);
while (mpz_sgn(m_tmp) != 0) {
mpz_tdiv_r_2exp(m_tmp2, m_tmp, 32);
unsigned v = mpz_get_ui(m_tmp2);
digits.push_back(v);
mpz_tdiv_q_2exp(m_tmp, m_tmp, 32);
}
return r;
bool r = is_neg(a);
mpz_set(m_tmp, *a.m_ptr);
mpz_abs(m_tmp, m_tmp);
while (mpz_sgn(m_tmp) != 0) {
mpz_tdiv_r_2exp(m_tmp2, m_tmp, 32);
unsigned v = mpz_get_ui(m_tmp2);
digits.push_back(v);
mpz_tdiv_q_2exp(m_tmp, m_tmp, 32);
}
return r;
#endif
}
}