mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

Merge remote-tracking branch 'upstream/master' into HEAD

Browse source
This commit is contained in:
Murphy Berzish 2017-10-30 13:55:31 -04:00
commit a8d025f5b4
1661 changed files with 45439 additions and 28238 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/CMakeLists.txt
View file

@ -75,7 +75,7 @@ z3_add_component(smt
normal_forms
parser_util
pattern
proof_checker
proofs
proto_model
simplex
substitution

13
src/smt/arith_eq_adapter.cpp
View file

@ -17,13 +17,12 @@ Revision History:
--*/
#include"smt_context.h"
#include"arith_eq_adapter.h"
#include"ast_pp.h"
#include"ast_ll_pp.h"
#include"stats.h"
#include"simplifier.h"
#include"ast_smt2_pp.h"
#include "smt/smt_context.h"
#include "smt/arith_eq_adapter.h"
#include "ast/ast_pp.h"
#include "ast/ast_ll_pp.h"
#include "util/stats.h"
#include "ast/ast_smt2_pp.h"
namespace smt {

9
src/smt/arith_eq_adapter.h
View file

@ -19,11 +19,10 @@ Revision History:
#ifndef ARITH_EQ_ADAPTER_H_
#define ARITH_EQ_ADAPTER_H_
#include"smt_theory.h"
#include"obj_pair_hashtable.h"
#include"arith_decl_plugin.h"
#include"statistics.h"
#include"arith_simplifier_plugin.h"
#include "smt/smt_theory.h"
#include "util/obj_pair_hashtable.h"
#include "ast/arith_decl_plugin.h"
#include "util/statistics.h"
namespace smt {

2
src/smt/arith_eq_solver.cpp
View file

@ -14,7 +14,7 @@ Author:
Nikolaj Bjorner (nbjorner) 2012-02-25
--*/
#include"arith_eq_solver.h"
#include "smt/arith_eq_solver.h"
arith_eq_solver::~arith_eq_solver() {

4
src/smt/arith_eq_solver.h
View file

@ -17,8 +17,8 @@ Author:
#ifndef ARITH_EQ_SOLVER_H_
#define ARITH_EQ_SOLVER_H_
#include"arith_decl_plugin.h"
#include"arith_rewriter.h"
#include "ast/arith_decl_plugin.h"
#include "ast/rewriter/arith_rewriter.h"
/**
\brief Simplifier for the arith family.

1015
src/smt/asserted_formulas.cpp
View file

File diff suppressed because it is too large Load diff

267
src/smt/asserted_formulas.h
View file

@ -19,87 +19,215 @@ Revision History:
#ifndef ASSERTED_FORMULAS_H_
#define ASSERTED_FORMULAS_H_
#include"smt_params.h"
#include"simplifier.h"
#include"basic_simplifier_plugin.h"
#include"static_features.h"
#include"macro_manager.h"
#include"macro_finder.h"
#include"defined_names.h"
#include"maximise_ac_sharing.h"
#include"bit2int.h"
#include"statistics.h"
#include"pattern_inference.h"
#include "util/statistics.h"
#include "ast/static_features.h"
#include "ast/expr_substitution.h"
#include "ast/rewriter/th_rewriter.h"
#include "ast/rewriter/bit2int.h"
#include "ast/rewriter/maximize_ac_sharing.h"
#include "ast/rewriter/distribute_forall.h"
#include "ast/rewriter/pull_ite_tree.h"
#include "ast/rewriter/push_app_ite.h"
#include "ast/rewriter/inj_axiom.h"
#include "ast/rewriter/bv_elim.h"
#include "ast/rewriter/der.h"
#include "ast/rewriter/elim_bounds.h"
#include "ast/macros/macro_manager.h"
#include "ast/macros/macro_finder.h"
#include "ast/normal_forms/defined_names.h"
#include "ast/normal_forms/pull_quant.h"
#include "ast/pattern/pattern_inference.h"
#include "smt/params/smt_params.h"
#include "smt/elim_term_ite.h"
class arith_simplifier_plugin;
class bv_simplifier_plugin;
class asserted_formulas {
ast_manager & m;
smt_params & m_params;
simplifier m_pre_simplifier;
simplifier m_simplifier;
basic_simplifier_plugin * m_bsimp;
bv_simplifier_plugin * m_bvsimp;
defined_names m_defined_names;
static_features m_static_features;
expr_ref_vector m_asserted_formulas; // formulas asserted by user
proof_ref_vector m_asserted_formula_prs; // proofs for the asserted formulas.
unsigned m_asserted_qhead;
macro_manager m_macro_manager;
scoped_ptr<macro_finder> m_macro_finder;
bit2int m_bit2int;
maximise_bv_sharing m_bv_sharing;
ast_manager & m;
smt_params & m_params;
th_rewriter m_rewriter;
expr_substitution m_substitution;
scoped_expr_substitution m_scoped_substitution;
defined_names m_defined_names;
static_features m_static_features;
vector<justified_expr> m_formulas;
unsigned m_qhead;
bool m_elim_and;
macro_manager m_macro_manager;
scoped_ptr<macro_finder> m_macro_finder;
maximize_bv_sharing_rw m_bv_sharing;
bool m_inconsistent;
bool m_has_quantifiers;
struct scope {
unsigned m_asserted_formulas_lim;
unsigned m_formulas_lim;
bool m_inconsistent_old;
};
svector<scope> m_scopes;
obj_map<expr, unsigned> m_expr2depth;
class simplify_fmls {
protected:
asserted_formulas& af;
ast_manager& m;
char const* m_id;
public:
simplify_fmls(asserted_formulas& af, char const* id): af(af), m(af.m), m_id(id) {}
char const* id() const { return m_id; }
virtual void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) = 0;
virtual bool should_apply() const { return true;}
virtual void post_op() {}
virtual void operator()();
};
class reduce_asserted_formulas_fn : public simplify_fmls {
public:
reduce_asserted_formulas_fn(asserted_formulas& af): simplify_fmls(af, "reduce-asserted") {}
virtual void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) { af.m_rewriter(j.get_fml(), n, p); }
};
class find_macros_fn : public simplify_fmls {
public:
find_macros_fn(asserted_formulas& af): simplify_fmls(af, "find-macros") {}
virtual void operator()() { af.find_macros_core(); }
virtual bool should_apply() const { return af.m_params.m_macro_finder && af.has_quantifiers(); }
virtual void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) { UNREACHABLE(); }
};
class apply_quasi_macros_fn : public simplify_fmls {
public:
apply_quasi_macros_fn(asserted_formulas& af): simplify_fmls(af, "find-quasi-macros") {}
virtual void operator()() { af.apply_quasi_macros(); }
virtual bool should_apply() const { return af.m_params.m_quasi_macros && af.has_quantifiers(); }
virtual void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) { UNREACHABLE(); }
};
class nnf_cnf_fn : public simplify_fmls {
public:
nnf_cnf_fn(asserted_formulas& af): simplify_fmls(af, "nnf-cnf") {}
virtual void operator()() { af.nnf_cnf(); }
virtual bool should_apply() const { return af.m_params.m_nnf_cnf || (af.m_params.m_mbqi && af.has_quantifiers()); }
virtual void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) { UNREACHABLE(); }
};
class propagate_values_fn : public simplify_fmls {
public:
propagate_values_fn(asserted_formulas& af): simplify_fmls(af, "propagate-values") {}
virtual void operator()() { af.propagate_values(); }
virtual bool should_apply() const { return af.m_params.m_propagate_values; }
virtual void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) { UNREACHABLE(); }
};
class distribute_forall_fn : public simplify_fmls {
distribute_forall m_functor;
public:
distribute_forall_fn(asserted_formulas& af): simplify_fmls(af, "distribute-forall"), m_functor(af.m) {}
virtual void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) { m_functor(j.get_fml(), n); }
virtual bool should_apply() const { return af.m_params.m_distribute_forall && af.has_quantifiers(); }
virtual void post_op() { af.reduce_and_solve(); TRACE("asserted_formulas", af.display(tout);); }
};
class pattern_inference_fn : public simplify_fmls {
pattern_inference_rw m_infer;
public:
pattern_inference_fn(asserted_formulas& af): simplify_fmls(af, "pattern-inference"), m_infer(af.m, af.m_params) {}
virtual void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) { m_infer(j.get_fml(), n, p); }
virtual bool should_apply() const { return af.m_params.m_ematching && af.has_quantifiers(); }
};
class refine_inj_axiom_fn : public simplify_fmls {
public:
refine_inj_axiom_fn(asserted_formulas& af): simplify_fmls(af, "refine-injectivity") {}
virtual void simplify(justified_expr const& j, expr_ref& n, proof_ref& p);
virtual bool should_apply() const { return af.m_params.m_refine_inj_axiom && af.has_quantifiers(); }
};
class max_bv_sharing_fn : public simplify_fmls {
public:
max_bv_sharing_fn(asserted_formulas& af): simplify_fmls(af, "maximizing-bv-sharing") {}
virtual void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) { af.m_bv_sharing(j.get_fml(), n, p); }
virtual bool should_apply() const { return af.m_params.m_max_bv_sharing; }
virtual void post_op() { af.m_reduce_asserted_formulas(); }
};
class elim_term_ite_fn : public simplify_fmls {
elim_term_ite_rw m_elim;
public:
elim_term_ite_fn(asserted_formulas& af): simplify_fmls(af, "elim-term-ite"), m_elim(af.m, af.m_defined_names) {}
virtual void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) { m_elim(j.get_fml(), n, p); }
virtual bool should_apply() const { return af.m_params.m_eliminate_term_ite && af.m_params.m_lift_ite != LI_FULL; }
virtual void post_op() { af.m_formulas.append(m_elim.new_defs()); af.reduce_and_solve(); m_elim.reset(); }
};
#define MK_SIMPLIFIERA(NAME, FUNCTOR, MSG, APP, ARG, REDUCE) \
class NAME : public simplify_fmls { \
FUNCTOR m_functor; \
public: \
NAME(asserted_formulas& af):simplify_fmls(af, MSG), m_functor ARG {} \
virtual void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) { \
m_functor(j.get_fml(), n, p); \
} \
virtual void post_op() { if (REDUCE) af.reduce_and_solve(); } \
virtual bool should_apply() const { return APP; } \
}; \
#define MK_SIMPLIFIERF(NAME, FUNCTOR, MSG, APP, REDUCE) MK_SIMPLIFIERA(NAME, FUNCTOR, MSG, APP, (af.m), REDUCE)
MK_SIMPLIFIERF(pull_cheap_ite_trees, pull_cheap_ite_tree_rw, "pull-cheap-ite-trees", af.m_params.m_pull_cheap_ite_trees, false);
MK_SIMPLIFIERF(pull_nested_quantifiers, pull_nested_quant, "pull-nested-quantifiers", af.m_params.m_pull_nested_quantifiers && af.has_quantifiers(), false);
MK_SIMPLIFIERF(cheap_quant_fourier_motzkin, elim_bounds_rw, "cheap-fourier-motzkin", af.m_params.m_eliminate_bounds && af.has_quantifiers(), true);
MK_SIMPLIFIERF(elim_bvs_from_quantifiers, bv_elim_rw, "eliminate-bit-vectors-from-quantifiers", af.m_params.m_bb_quantifiers, true);
MK_SIMPLIFIERF(apply_bit2int, bit2int, "propagate-bit-vector-over-integers", af.m_params.m_simplify_bit2int, true);
MK_SIMPLIFIERA(lift_ite, push_app_ite_rw, "lift-ite", af.m_params.m_lift_ite != LI_NONE, (af.m, af.m_params.m_lift_ite == LI_CONSERVATIVE), true);
MK_SIMPLIFIERA(ng_lift_ite, ng_push_app_ite_rw, "lift-ite", af.m_params.m_ng_lift_ite != LI_NONE, (af.m, af.m_params.m_ng_lift_ite == LI_CONSERVATIVE), true);
reduce_asserted_formulas_fn m_reduce_asserted_formulas;
distribute_forall_fn m_distribute_forall;
pattern_inference_fn m_pattern_inference;
refine_inj_axiom_fn m_refine_inj_axiom;
max_bv_sharing_fn m_max_bv_sharing_fn;
elim_term_ite_fn m_elim_term_ite;
pull_cheap_ite_trees m_pull_cheap_ite_trees;
pull_nested_quantifiers m_pull_nested_quantifiers;
elim_bvs_from_quantifiers m_elim_bvs_from_quantifiers;
cheap_quant_fourier_motzkin m_cheap_quant_fourier_motzkin;
apply_bit2int m_apply_bit2int;
lift_ite m_lift_ite;
ng_lift_ite m_ng_lift_ite;
find_macros_fn m_find_macros;
propagate_values_fn m_propagate_values;
nnf_cnf_fn m_nnf_cnf;
apply_quasi_macros_fn m_apply_quasi_macros;
bool invoke(simplify_fmls& s);
void swap_asserted_formulas(vector<justified_expr>& new_fmls);
void push_assertion(expr * e, proof * pr, vector<justified_expr>& result);
bool canceled() { return m.canceled(); }
bool check_well_sorted() const;
unsigned get_total_size() const;
void setup_simplifier_plugins(simplifier & s, basic_simplifier_plugin * & bsimp, arith_simplifier_plugin * & asimp, bv_simplifier_plugin * & bvsimp);
void reduce_asserted_formulas();
void swap_asserted_formulas(expr_ref_vector & new_exprs, proof_ref_vector & new_prs);
void find_macros_core();
void find_macros();
void expand_macros();
void apply_quasi_macros();
void nnf_cnf();
void infer_patterns();
void eliminate_term_ite();
void reduce_and_solve();
void flush_cache() { m_pre_simplifier.reset(); m_simplifier.reset(); }
void flush_cache() { m_rewriter.reset(); m_rewriter.set_substitution(&m_substitution); }
void set_eliminate_and(bool flag);
void propagate_values();
void propagate_booleans();
unsigned propagate_values(unsigned i);
void update_substitution(expr* n, proof* p);
bool is_gt(expr* lhs, expr* rhs);
void compute_depth(expr* e);
unsigned depth(expr* e) { return m_expr2depth[e]; }
bool pull_cheap_ite_trees();
bool pull_nested_quantifiers();
void push_assertion(expr * e, proof * pr, expr_ref_vector & result, proof_ref_vector & result_prs);
void eliminate_and();
void refine_inj_axiom();
bool cheap_quant_fourier_motzkin();
void apply_distribute_forall();
bool apply_bit2int();
void lift_ite();
bool elim_bvs_from_quantifiers();
void ng_lift_ite();
#ifdef Z3DEBUG
bool check_well_sorted() const;
#endif
unsigned get_total_size() const;
bool has_bv() const;
void max_bv_sharing();
bool canceled() { return m.canceled(); }
void init(unsigned num_formulas, expr * const * formulas, proof * const * prs);
public:
asserted_formulas(ast_manager & m, smt_params & p);
~asserted_formulas();
bool has_quantifiers() const { return m_has_quantifiers; }
void setup();
void assert_expr(expr * e, proof * in_pr);
void assert_expr(expr * e);
@ -109,26 +237,20 @@ public:
bool inconsistent() const { return m_inconsistent; }
proof * get_inconsistency_proof() const;
void reduce();
unsigned get_num_formulas() const { return m_asserted_formulas.size(); }
unsigned get_num_formulas() const { return m_formulas.size(); }
unsigned get_formulas_last_level() const;
unsigned get_qhead() const { return m_asserted_qhead; }
unsigned get_qhead() const { return m_qhead; }
void commit();
void commit(unsigned new_qhead);
expr * get_formula(unsigned idx) const { return m_asserted_formulas.get(idx); }
proof * get_formula_proof(unsigned idx) const { return m.proofs_enabled() ? m_asserted_formula_prs.get(idx) : 0; }
expr * const * get_formulas() const { return m_asserted_formulas.c_ptr(); }
proof * const * get_formula_proofs() const { return m_asserted_formula_prs.c_ptr(); }
void init(unsigned num_formulas, expr * const * formulas, proof * const * prs);
void register_simplifier_plugin(simplifier_plugin * p) { m_simplifier.register_plugin(p); }
simplifier & get_simplifier() { return m_simplifier; }
void get_assertions(ptr_vector<expr> & result);
bool empty() const { return m_asserted_formulas.empty(); }
void collect_static_features();
expr * get_formula(unsigned idx) const { return m_formulas[idx].get_fml(); }
proof * get_formula_proof(unsigned idx) const { return m_formulas[idx].get_proof(); }
th_rewriter & get_rewriter() { return m_rewriter; }
void get_assertions(ptr_vector<expr> & result) const;
bool empty() const { return m_formulas.empty(); }
void display(std::ostream & out) const;
void display_ll(std::ostream & out, ast_mark & pp_visited) const;
void collect_statistics(statistics & st) const;
// TODO: improve precision of the following method.
bool has_quantifiers() const { return m_simplifier.visited_quantifier(); /* approximation */ }
// -----------------------------------
//
@ -142,6 +264,7 @@ public:
quantifier * get_macro_quantifier(func_decl * f) const { return m_macro_manager.get_macro_quantifier(f); }
// auxiliary function used to create a logic context based on a model.
void insert_macro(func_decl * f, quantifier * m, proof * pr) { m_macro_manager.insert(f, m, pr); }
void insert_macro(func_decl * f, quantifier * m, proof * pr, expr_dependency* dep) { m_macro_manager.insert(f, m, pr, dep); }
};

2
src/smt/cached_var_subst.cpp
View file

@ -16,7 +16,7 @@ Author:
Revision History:
--*/
#include"cached_var_subst.h"
#include "smt/cached_var_subst.h"
bool cached_var_subst::key_eq_proc::operator()(cached_var_subst::key * k1, cached_var_subst::key * k2) const {
if (k1->m_qa != k2->m_qa)

6
src/smt/cached_var_subst.h
View file

@ -19,9 +19,9 @@ Revision History:
#ifndef CACHED_VAR_SUBST_H_
#define CACHED_VAR_SUBST_H_
#include"var_subst.h"
#include"map.h"
#include"smt_enode.h"
#include "ast/rewriter/var_subst.h"
#include "util/map.h"
#include "smt/smt_enode.h"
class cached_var_subst {
struct key {

4
src/smt/cost_evaluator.cpp
View file

@ -16,8 +16,8 @@ Author:
Revision History:
--*/
#include"cost_evaluator.h"
#include"warning.h"
#include "smt/cost_evaluator.h"
#include "util/warning.h"
cost_evaluator::cost_evaluator(ast_manager & m):
m_manager(m),

4
src/smt/cost_evaluator.h
View file

@ -19,8 +19,8 @@ Revision History:
#ifndef COST_EVALUATOR_H_
#define COST_EVALUATOR_H_
#include"ast.h"
#include"arith_decl_plugin.h"
#include "ast/ast.h"
#include "ast/arith_decl_plugin.h"
class cost_evaluator {
ast_manager & m_manager;

2
src/smt/database.smt
View file

@ -11,7 +11,7 @@
:formula (forall (a Int) (i Int) (e Int)
(= (?select (?store a i e) i) e)
:pats { (?store a i e) }
:weight { 0 })
:weight { 0 })
:formula (forall (a Int) (i Int) (j Int) (e Int)
(or (= i j) (= (?select (?store a i e) j) (?select a j)))

74
src/smt/diff_logic.h
View file

@ -19,12 +19,12 @@ Revision History:
#ifndef DIFF_LOGIC_H_
#define DIFF_LOGIC_H_
#include"vector.h"
#include"heap.h"
#include"statistics.h"
#include"trace.h"
#include"warning.h"
#include"uint_set.h"
#include "util/vector.h"
#include "util/heap.h"
#include "util/statistics.h"
#include "util/trace.h"
#include "util/warning.h"
#include "util/uint_set.h"
#include<deque>
typedef int dl_var;
@ -956,8 +956,8 @@ public:
}
void get_neighbours_undirected(dl_var current, svector<dl_var> & neighbours) {
neighbours.reset();
edge_id_vector & out_edges = m_out_edges[current];
neighbours.reset();
edge_id_vector & out_edges = m_out_edges[current];
typename edge_id_vector::iterator it = out_edges.begin(), end = out_edges.end();
for (; it != end; ++it) {
edge_id e_id = *it;
@ -968,7 +968,7 @@ public:
}
edge_id_vector & in_edges = m_in_edges[current];
typename edge_id_vector::iterator it2 = in_edges.begin(), end2 = in_edges.end();
for (; it2 != end2; ++it2) {
for (; it2 != end2; ++it2) {
edge_id e_id = *it2;
edge & e = m_edges[e_id];
SASSERT(e.get_target() == current);
@ -980,19 +980,19 @@ public:
void dfs_undirected(dl_var start, svector<dl_var> & threads) {
threads.reset();
threads.resize(get_num_nodes());
uint_set discovered, explored;
svector<dl_var> nodes;
uint_set discovered, explored;
svector<dl_var> nodes;
discovered.insert(start);
nodes.push_back(start);
dl_var prev = start;
while(!nodes.empty()) {
dl_var current = nodes.back();
nodes.push_back(start);
dl_var prev = start;
while(!nodes.empty()) {
dl_var current = nodes.back();
SASSERT(discovered.contains(current) && !explored.contains(current));
svector<dl_var> neighbours;
get_neighbours_undirected(current, neighbours);
svector<dl_var> neighbours;
get_neighbours_undirected(current, neighbours);
SASSERT(!neighbours.empty());
bool found = false;
for (unsigned i = 0; i < neighbours.size(); ++i) {
for (unsigned i = 0; i < neighbours.size(); ++i) {
dl_var next = neighbours[i];
DEBUG_CODE(
edge_id id;
@ -1002,18 +1002,18 @@ public:
threads[prev] = next;
prev = next;
discovered.insert(next);
nodes.push_back(next);
nodes.push_back(next);
found = true;
break;
}
}
}
SASSERT(!nodes.empty());
if (!found) {
explored.insert(current);
nodes.pop_back();
}
}
threads[prev] = start;
}
threads[prev] = start;
}
void bfs_undirected(dl_var start, svector<dl_var> & parents, svector<dl_var> & depths) {
@ -1022,31 +1022,31 @@ public:
parents[start] = -1;
depths.reset();
depths.resize(get_num_nodes());
uint_set visited;
std::deque<dl_var> nodes;
visited.insert(start);
nodes.push_front(start);
while(!nodes.empty()) {
uint_set visited;
std::deque<dl_var> nodes;
visited.insert(start);
nodes.push_front(start);
while(!nodes.empty()) {
dl_var current = nodes.back();
nodes.pop_back();
SASSERT(visited.contains(current));
SASSERT(visited.contains(current));
svector<dl_var> neighbours;
get_neighbours_undirected(current, neighbours);
get_neighbours_undirected(current, neighbours);
SASSERT(!neighbours.empty());
for (unsigned i = 0; i < neighbours.size(); ++i) {
dl_var next = neighbours[i];
for (unsigned i = 0; i < neighbours.size(); ++i) {
dl_var next = neighbours[i];
DEBUG_CODE(
edge_id id;
SASSERT(get_edge_id(current, next, id) || get_edge_id(next, current, id)););
if (!visited.contains(next)) {
TRACE("diff_logic", tout << "parents[" << next << "] --> " << current << std::endl;);
parents[next] = current;
depths[next] = depths[current] + 1;
visited.insert(next);
nodes.push_front(next);
parents[next] = current;
depths[next] = depths[current] + 1;
visited.insert(next);
nodes.push_front(next);
}
}
}
}
}
}
template<typename Functor>

6
src/smt/dyn_ack.cpp
View file

@ -16,9 +16,9 @@ Author:
Revision History:
--*/
#include"smt_context.h"
#include"dyn_ack.h"
#include"ast_pp.h"
#include "smt/smt_context.h"
#include "smt/dyn_ack.h"
#include "ast/ast_pp.h"
namespace smt {

12
src/smt/dyn_ack.h
View file

@ -19,12 +19,12 @@ Revision History:
#ifndef DYN_ACK_H_
#define DYN_ACK_H_
#include"ast.h"
#include"dyn_ack_params.h"
#include"obj_hashtable.h"
#include"obj_pair_hashtable.h"
#include"obj_triple_hashtable.h"
#include"smt_clause.h"
#include "ast/ast.h"
#include "smt/params/dyn_ack_params.h"
#include "util/obj_hashtable.h"
#include "util/obj_pair_hashtable.h"
#include "util/obj_triple_hashtable.h"
#include "smt/smt_clause.h"
namespace smt {

156
src/smt/elim_term_ite.cpp
View file

@ -16,145 +16,25 @@ Author:
Revision History:
--*/
#include"elim_term_ite.h"
#include"ast_smt2_pp.h"
#include "smt/elim_term_ite.h"
#include "ast/ast_smt2_pp.h"
void elim_term_ite::operator()(expr * n,
expr_ref_vector & new_defs,
proof_ref_vector & new_def_proofs,
expr_ref & r,
proof_ref & pr) {
m_coarse_proofs.reset();
m_new_defs = &new_defs;
m_new_def_proofs = &new_def_proofs;
reduce_core(n);
expr * r2;
proof * pr2;
get_cached(n, r2, pr2);
r = r2;
switch (m.proof_mode()) {
case PGM_DISABLED:
pr = m.mk_undef_proof();
break;
case PGM_COARSE:
remove_duplicates(m_coarse_proofs);
pr = n == r2 ? m.mk_oeq_reflexivity(n) : m.mk_apply_defs(n, r, m_coarse_proofs.size(), m_coarse_proofs.c_ptr());
break;
case PGM_FINE:
pr = pr2 == 0 ? m.mk_oeq_reflexivity(n) : pr2;
break;
br_status elim_term_ite_cfg::reduce_app(func_decl* f, unsigned n, expr * const* args, expr_ref& result, proof_ref& result_pr) {
if (!m.is_term_ite(f)) {
return BR_FAILED;
}
m_coarse_proofs.reset();
expr_ref new_def(m);
proof_ref new_def_pr(m);
app_ref r(m.mk_app(f, n, args), m);
app_ref new_r(m);
if (!m_defined_names.mk_name(r, new_def, new_def_pr, new_r, result_pr)) {
return BR_FAILED;
}
result = new_r;
CTRACE("elim_term_ite_bug", new_def.get() == 0, tout << mk_ismt2_pp(r, m) << "\n";);
m_new_defs.push_back(justified_expr(m, new_def, new_def_pr));
return BR_DONE;
}
void elim_term_ite::reduce_core(expr * n) {
m_todo.reset();
if (!is_cached(n)) {
m_todo.push_back(n);
while (!m_todo.empty()) {
expr * n = m_todo.back();
if (is_cached(n)) {
m_todo.pop_back();
}
else if (visit_children(n)) {
m_todo.pop_back();
reduce1(n);
}
}
}
}
bool elim_term_ite::visit_children(expr * n) {
bool visited = true;
unsigned j;
switch(n->get_kind()) {
case AST_VAR:
return true;
case AST_APP:
j = to_app(n)->get_num_args();
while (j > 0) {
--j;
visit(to_app(n)->get_arg(j), visited);
}
return visited;
case AST_QUANTIFIER:
visit(to_quantifier(n)->get_expr(), visited);
return visited;
default:
UNREACHABLE();
return true;
}
}
void elim_term_ite::reduce1(expr * n) {
switch (n->get_kind()) {
case AST_VAR:
cache_result(n, n, 0);
break;
case AST_APP:
reduce1_app(to_app(n));
break;
case AST_QUANTIFIER:
reduce1_quantifier(to_quantifier(n));
break;
default:
UNREACHABLE();
}
}
void elim_term_ite::reduce1_app(app * n) {
m_args.reset();
func_decl * decl = n->get_decl();
proof_ref p1(m);
get_args(n, m_args, p1);
if (!m.fine_grain_proofs())
p1 = 0;
expr_ref r(m);
r = m.mk_app(decl, m_args.size(), m_args.c_ptr());
if (m.is_term_ite(r)) {
expr_ref new_def(m);
proof_ref new_def_pr(m);
app_ref new_r(m);
proof_ref new_pr(m);
if (m_defined_names.mk_name(r, new_def, new_def_pr, new_r, new_pr)) {
CTRACE("elim_term_ite_bug", new_def.get() == 0, tout << mk_ismt2_pp(r, m) << "\n";);
SASSERT(new_def.get() != 0);
m_new_defs->push_back(new_def);
if (m.fine_grain_proofs()) {
m_new_def_proofs->push_back(new_def_pr);
new_pr = m.mk_transitivity(p1, new_pr);
}
else {
// [Leo] This looks fishy... why do we add 0 into m_coarse_proofs when fine_grain_proofs are disabled?
new_pr = 0;
if (m.proofs_enabled())
m_coarse_proofs.push_back(new_pr);
}
}
else {
SASSERT(new_def.get() == 0);
if (!m.fine_grain_proofs())
new_pr = 0;
}
cache_result(n, new_r, new_pr);
}
else {
cache_result(n, r, p1);
}
}
void elim_term_ite::reduce1_quantifier(quantifier * q) {
expr * new_body;
proof * new_body_pr;
get_cached(q->get_expr(), new_body, new_body_pr);
quantifier * new_q = m.update_quantifier(q, new_body);
proof * p = q == new_q ? 0 : m.mk_oeq_quant_intro(q, new_q, new_body_pr);
cache_result(q, new_q, p);
}

48
src/smt/elim_term_ite.h
View file

@ -19,32 +19,36 @@ Revision History:
#ifndef ELIM_TERM_ITE_H_
#define ELIM_TERM_ITE_H_
#include"simplifier.h"
#include"defined_names.h"
#include "ast/normal_forms/defined_names.h"
#include "ast/rewriter/rewriter.h"
#include "ast/justified_expr.h"
class elim_term_ite : public simplifier {
defined_names & m_defined_names;
proof_ref_vector m_coarse_proofs;
expr_ref_vector * m_new_defs;
proof_ref_vector * m_new_def_proofs;
void reduce_core(expr * n);
bool visit_children(expr * n);
void reduce1(expr * n);
void reduce1_app(app * n);
void reduce1_quantifier(quantifier * q);
class elim_term_ite_cfg : public default_rewriter_cfg {
ast_manager& m;
defined_names & m_defined_names;
vector<justified_expr> m_new_defs;
public:
elim_term_ite(ast_manager & m, defined_names & d):simplifier(m), m_defined_names(d), m_coarse_proofs(m) {
m_use_oeq = true;
enable_ac_support(false);
elim_term_ite_cfg(ast_manager & m, defined_names & d): m(m), m_defined_names(d) {
// TBD enable_ac_support(false);
}
virtual ~elim_term_ite() {}
void operator()(expr * n, // [IN]
expr_ref_vector & new_defs, // [OUT] new definitions
proof_ref_vector & new_def_proofs, // [OUT] proofs of the new definitions
expr_ref & r, // [OUT] resultant expression
proof_ref & pr // [OUT] proof for (~ n r)
);
virtual ~elim_term_ite_cfg() {}
vector<justified_expr> const& new_defs() const { return m_new_defs; }
void reset() { m_new_defs.reset(); }
br_status reduce_app(func_decl* f, unsigned n, expr *const* args, expr_ref& result, proof_ref& result_pr);
};
class elim_term_ite_rw : public rewriter_tpl<elim_term_ite_cfg> {
elim_term_ite_cfg m_cfg;
public:
elim_term_ite_rw(ast_manager& m, defined_names & dn):
rewriter_tpl<elim_term_ite_cfg>(m, m.proofs_enabled(), m_cfg),
m_cfg(m, dn)
{}
vector<justified_expr> const& new_defs() const { return m_cfg.new_defs(); }
void reset() { m_cfg.reset(); }
};
#endif /* ELIM_TERM_ITE_H_ */

10
src/smt/expr_context_simplifier.cpp
View file

@ -17,11 +17,11 @@ Revision History:
--*/
#include "expr_context_simplifier.h"
#include "ast_pp.h"
#include "obj_hashtable.h"
#include "smt_kernel.h"
#include "for_each_expr.h"
#include "smt/expr_context_simplifier.h"
#include "ast/ast_pp.h"
#include "util/obj_hashtable.h"
#include "smt/smt_kernel.h"
#include "ast/for_each_expr.h"
// table lookup before/after simplification.

14
src/smt/expr_context_simplifier.h
View file

@ -19,12 +19,12 @@ Revision History:
#ifndef EXPR_CONTEXT_SIMPLIFIER_H_
#define EXPR_CONTEXT_SIMPLIFIER_H_
#include "ast.h"
#include "obj_hashtable.h"
#include "basic_simplifier_plugin.h"
#include "smt_params.h"
#include "smt_kernel.h"
#include "arith_decl_plugin.h"
#include "ast/ast.h"
#include "util/obj_hashtable.h"
#include "smt/params/smt_params.h"
#include "smt/smt_kernel.h"
#include "ast/arith_decl_plugin.h"
#include "ast/rewriter/bool_rewriter.h"
class expr_context_simplifier {
typedef obj_map<expr, bool> context_map;
@ -33,7 +33,7 @@ class expr_context_simplifier {
arith_util m_arith;
context_map m_context;
expr_ref_vector m_trail;
basic_simplifier_plugin m_simp;
bool_rewriter m_simp;
expr_mark m_mark;
bool m_forward;
public:

2
src/smt/fingerprints.cpp
View file

@ -16,7 +16,7 @@ Author:
Revision History:
--*/
#include"fingerprints.h"
#include "smt/fingerprints.h"
namespace smt {

2
src/smt/fingerprints.h
View file

@ -19,7 +19,7 @@ Revision History:
#ifndef FINGERPRINTS_H_
#define FINGERPRINTS_H_
#include"smt_enode.h"
#include "smt/smt_enode.h"
namespace smt {

531
src/smt/mam.cpp
View file

File diff suppressed because it is too large Load diff

4
src/smt/mam.h
View file

@ -19,8 +19,8 @@ Revision History:
#ifndef MAM_H_
#define MAM_H_
#include"ast.h"
#include"smt_types.h"
#include "ast/ast.h"
#include "smt/smt_types.h"
namespace smt {
/**

2
src/smt/old_interval.cpp
View file

@ -17,7 +17,7 @@ Revision History:
--*/
#include"old_interval.h"
#include "smt/old_interval.h"
void ext_numeral::neg() {
switch (m_kind) {

4
src/smt/old_interval.h
View file

@ -19,8 +19,8 @@ Revision History:
#ifndef OLD_INTERVAL_H_
#define OLD_INTERVAL_H_
#include"rational.h"
#include"dependency.h"
#include "util/rational.h"
#include "util/dependency.h"
class ext_numeral {
public:

1
src/smt/params/CMakeLists.txt
View file

@ -13,7 +13,6 @@ z3_add_component(smt_params
ast
bit_blaster
pattern
simplifier
PYG_FILES
smt_params_helper.pyg
)

4
src/smt/params/dyn_ack_params.cpp
View file

@ -16,8 +16,8 @@ Author:
Revision History:
--*/
#include"dyn_ack_params.h"
#include"smt_params_helper.hpp"
#include "smt/params/dyn_ack_params.h"
#include "smt/params/smt_params_helper.hpp"
void dyn_ack_params::updt_params(params_ref const & _p) {
smt_params_helper p(_p);

2
src/smt/params/dyn_ack_params.h
View file

@ -19,7 +19,7 @@ Revision History:
#ifndef DYN_ACK_PARAMS_H_
#define DYN_ACK_PARAMS_H_
#include"params.h"
#include "util/params.h"
enum dyn_ack_strategy {
DACK_DISABLED,

11
src/smt/params/preprocessor_params.cpp
View file

@ -16,20 +16,20 @@ Author:
Revision History:
--*/
#include"preprocessor_params.h"
#include"smt_params_helper.hpp"
#include "smt/params/preprocessor_params.h"
#include "smt/params/smt_params_helper.hpp"
void preprocessor_params::updt_local_params(params_ref const & _p) {
smt_params_helper p(_p);
m_macro_finder = p.macro_finder();
m_quasi_macros = p.quasi_macros();
m_restricted_quasi_macros = p.restricted_quasi_macros();
m_pull_nested_quantifiers = p.pull_nested_quantifiers();
m_refine_inj_axiom = p.refine_inj_axioms();
}
void preprocessor_params::updt_params(params_ref const & p) {
pattern_inference_params::updt_params(p);
bv_simplifier_params::updt_params(p);
arith_simplifier_params::updt_params(p);
updt_local_params(p);
}
@ -38,15 +38,12 @@ void preprocessor_params::updt_params(params_ref const & p) {
void preprocessor_params::display(std::ostream & out) const {
pattern_inference_params::display(out);
bit_blaster_params::display(out);
bv_simplifier_params::display(out);
arith_simplifier_params::display(out);
DISPLAY_PARAM(m_lift_ite);
DISPLAY_PARAM(m_ng_lift_ite);
DISPLAY_PARAM(m_pull_cheap_ite_trees);
DISPLAY_PARAM(m_pull_nested_quantifiers);
DISPLAY_PARAM(m_eliminate_term_ite);
DISPLAY_PARAM(m_eliminate_and);
DISPLAY_PARAM(m_macro_finder);
DISPLAY_PARAM(m_propagate_values);
DISPLAY_PARAM(m_propagate_booleans);

12
src/smt/params/preprocessor_params.h
View file

@ -19,10 +19,8 @@ Revision History:
#ifndef PREPROCESSOR_PARAMS_H_
#define PREPROCESSOR_PARAMS_H_
#include"pattern_inference_params.h"
#include"bit_blaster_params.h"
#include"bv_simplifier_params.h"
#include"arith_simplifier_params.h"
#include "ast/pattern/pattern_inference_params.h"
#include "ast/rewriter/bit_blaster/bit_blaster_params.h"
enum lift_ite_kind {
LI_NONE,
@ -31,15 +29,12 @@ enum lift_ite_kind {
};
struct preprocessor_params : public pattern_inference_params,
public bit_blaster_params,
public bv_simplifier_params,
public arith_simplifier_params {
public bit_blaster_params {
lift_ite_kind m_lift_ite;
lift_ite_kind m_ng_lift_ite; // lift ite for non ground terms
bool m_pull_cheap_ite_trees;
bool m_pull_nested_quantifiers;
bool m_eliminate_term_ite;
bool m_eliminate_and; // represent (and a b) as (not (or (not a) (not b)))
bool m_macro_finder;
bool m_propagate_values;
bool m_propagate_booleans;
@ -62,7 +57,6 @@ public:
m_pull_cheap_ite_trees(false),
m_pull_nested_quantifiers(false),
m_eliminate_term_ite(false),
m_eliminate_and(true),
m_macro_finder(false),
m_propagate_values(true),
m_propagate_booleans(false), // TODO << check peformance

4
src/smt/params/qi_params.cpp
View file

@ -16,8 +16,8 @@ Author:
Revision History:
--*/
#include"qi_params.h"
#include"smt_params_helper.hpp"
#include "smt/params/qi_params.h"
#include "smt/params/smt_params_helper.hpp"
void qi_params::updt_params(params_ref const & _p) {
smt_params_helper p(_p);

4
src/smt/params/qi_params.h
View file

@ -19,8 +19,8 @@ Revision History:
#ifndef QI_PARAMS_H_
#define QI_PARAMS_H_
#include"util.h"
#include"params.h"
#include "util/util.h"
#include "util/params.h"
enum quick_checker_mode {
MC_NO, // do not use (cheap) model checking based instantiation

11
src/smt/params/smt_params.cpp
View file

@ -16,10 +16,10 @@ Author:
Revision History:
--*/
#include"smt_params.h"
#include"smt_params_helper.hpp"
#include"model_params.hpp"
#include"gparams.h"
#include "smt/params/smt_params.h"
#include "smt/params/smt_params_helper.hpp"
#include "model/model_params.hpp"
#include "util/gparams.h"
void smt_params::updt_local_params(params_ref const & _p) {
smt_params_helper p(_p);
@ -49,6 +49,9 @@ void smt_params::updt_local_params(params_ref const & _p) {
else if (_p.get_bool("arith.least_error_pivot", false))
m_arith_pivot_strategy = ARITH_PIVOT_LEAST_ERROR;
theory_array_params::updt_params(_p);
m_dump_benchmarks = false;
m_dump_min_time = 0.5;
m_dump_recheck = false;
}
void smt_params::updt_params(params_ref const & p) {

62
src/smt/params/smt_params.h
View file

@ -19,19 +19,19 @@ Revision History:
#ifndef SMT_PARAMS_H_
#define SMT_PARAMS_H_
#include"ast.h"
#include"dyn_ack_params.h"
#include"qi_params.h"
#include"theory_arith_params.h"
#include"theory_array_params.h"
#include"theory_bv_params.h"
#include"theory_str_params.h"
#include"theory_pb_params.h"
#include"theory_datatype_params.h"
#include"preprocessor_params.h"
#include"context_params.h"
#include "ast/ast.h"
#include "smt/params/dyn_ack_params.h"
#include "smt/params/qi_params.h"
#include "smt/params/theory_arith_params.h"
#include "smt/params/theory_array_params.h"
#include "smt/params/theory_bv_params.h"
#include "smt/params/theory_str_params.h"
#include "smt/params/theory_pb_params.h"
#include "smt/params/theory_datatype_params.h"
#include "smt/params/preprocessor_params.h"
#include "cmd_context/context_params.h"
enum phase_selection {
enum phase_selection {
PS_ALWAYS_FALSE,
PS_ALWAYS_TRUE,
PS_CACHING,
@ -52,7 +52,8 @@ enum restart_strategy {
enum lemma_gc_strategy {
LGC_FIXED,
LGC_GEOMETRIC,
LGC_AT_RESTART
LGC_AT_RESTART,
LGC_NONE
};
enum initial_activity {
@ -71,11 +72,11 @@ enum case_split_strategy {
CS_ACTIVITY_THEORY_AWARE_BRANCHING // activity-based case split, but theory solvers can manipulate activity
};
struct smt_params : public preprocessor_params,
public dyn_ack_params,
public qi_params,
public theory_arith_params,
public theory_array_params,
struct smt_params : public preprocessor_params,
public dyn_ack_params,
public qi_params,
public theory_arith_params,
public theory_array_params,
public theory_bv_params,
public theory_str_params,
public theory_pb_params,
@ -153,12 +154,12 @@ struct smt_params : public preprocessor_params,
unsigned m_lemma_gc_initial;
double m_lemma_gc_factor;
unsigned m_new_old_ratio; //!< the ratio of new and old clauses.
unsigned m_new_clause_activity;
unsigned m_new_clause_activity;
unsigned m_old_clause_activity;
unsigned m_new_clause_relevancy; //!< Max. number of unassigned literals to be considered relevant.
unsigned m_old_clause_relevancy; //!< Max. number of unassigned literals to be considered relevant.
double m_inv_clause_decay; //!< clause activity decay
// -----------------------------------
//
// SMT-LIB (debug) pretty printer
@ -166,7 +167,7 @@ struct smt_params : public preprocessor_params,
// -----------------------------------
bool m_smtlib_dump_lemmas;
symbol m_logic;
// -----------------------------------
//
// Statistics for Profiling
@ -179,10 +180,10 @@ struct smt_params : public preprocessor_params,
// -----------------------------------
//
// Model generation
// Model generation
//
// -----------------------------------
bool m_model;
bool m_model;
bool m_model_compact;
bool m_model_on_timeout;
bool m_model_on_final_check;
@ -213,10 +214,19 @@ struct smt_params : public preprocessor_params,
unsigned m_timeout;
unsigned m_rlimit;
bool m_at_labels_cex; // only use labels which contains the @ symbol when building multiple counterexamples.
bool m_check_at_labels; // check that @ labels are inserted to generate unique counter-examples.
bool m_check_at_labels; // check that @ labels are inserted to generate unique counter-examples.
bool m_dump_goal_as_smt;
bool m_auto_config;
// -----------------------------------
//
// Spacer hacking
//
// -----------------------------------
bool m_dump_benchmarks;
double m_dump_min_time;
bool m_dump_recheck;
// -----------------------------------
//
// Solver selection
@ -228,7 +238,7 @@ struct smt_params : public preprocessor_params,
m_display_proof(false),
m_display_dot_proof(false),
m_display_unsat_core(false),
m_check_proof(false),
m_check_proof(false),
m_eq_propagation(true),
m_binary_clause_opt(true),
m_relevancy_lvl(2),
@ -270,7 +280,7 @@ struct smt_params : public preprocessor_params,
m_new_old_ratio(16),
m_new_clause_activity(10),
m_old_clause_activity(500),
m_new_clause_relevancy(45),
m_new_clause_relevancy(45),
m_old_clause_relevancy(6),
m_inv_clause_decay(1),
m_smtlib_dump_lemmas(false),

5
src/smt/params/smt_params_helper.pyg
View file

@ -7,6 +7,8 @@ def_module_params(module_name='smt',
('random_seed', UINT, 0, 'random seed for the smt solver'),
('relevancy', UINT, 2, 'relevancy propagation heuristic: 0 - disabled, 1 - relevancy is tracked by only affects quantifier instantiation, 2 - relevancy is tracked, and an atom is only asserted if it is relevant'),
('macro_finder', BOOL, False, 'try to find universally quantified formulas that can be viewed as macros'),
('quasi_macros', BOOL, False, 'try to find universally quantified formulas that are quasi-macros'),
('restricted_quasi_macros', BOOL, False, 'try to find universally quantified formulas that are restricted quasi-macros'),
('ematching', BOOL, True, 'E-Matching based quantifier instantiation'),
('phase_selection', UINT, 3, 'phase selection heuristic: 0 - always false, 1 - always true, 2 - phase caching, 3 - phase caching conservative, 4 - phase caching conservative 2, 5 - random, 6 - number of occurrences'),
('restart_strategy', UINT, 1, '0 - geometric, 1 - inner-outer-geometric, 2 - luby, 3 - fixed, 4 - arithmetic'),
@ -80,5 +82,6 @@ def_module_params(module_name='smt',
('core.minimize', BOOL, False, 'minimize unsat core produced by SMT context'),
('core.extend_patterns', BOOL, False, 'extend unsat core with literals that trigger (potential) quantifier instances'),
('core.extend_patterns.max_distance', UINT, UINT_MAX, 'limits the distance of a pattern-extended unsat core'),
('core.extend_nonlocal_patterns', BOOL, False, 'extend unsat cores with literals that have quantifiers with patterns that contain symbols which are not in the quantifier\'s body')
('core.extend_nonlocal_patterns', BOOL, False, 'extend unsat cores with literals that have quantifiers with patterns that contain symbols which are not in the quantifier\'s body'),
('lemma_gc_strategy', UINT, 0, 'lemma garbage collection strategy: 0 - fixed, 1 - geometric, 2 - at restart, 3 - none')
))

9
src/smt/params/theory_arith_params.cpp
View file

@ -16,8 +16,9 @@ Author:
Revision History:
--*/
#include"theory_arith_params.h"
#include"smt_params_helper.hpp"
#include "smt/params/theory_arith_params.h"
#include "smt/params/smt_params_helper.hpp"
#include "ast/rewriter/arith_rewriter_params.hpp"
void theory_arith_params::updt_params(params_ref const & _p) {
smt_params_helper p(_p);
@ -36,12 +37,16 @@ void theory_arith_params::updt_params(params_ref const & _p) {
m_arith_bound_prop = static_cast<bound_prop_mode>(p.arith_propagation_mode());
m_arith_dump_lemmas = p.arith_dump_lemmas();
m_arith_reflect = p.arith_reflect();
arith_rewriter_params ap(_p);
m_arith_eq2ineq = ap.eq2ineq();
}
#define DISPLAY_PARAM(X) out << #X"=" << X << std::endl;
void theory_arith_params::display(std::ostream & out) const {
DISPLAY_PARAM(m_arith_eq2ineq);
DISPLAY_PARAM(m_arith_process_all_eqs);
DISPLAY_PARAM(m_arith_mode);
DISPLAY_PARAM(m_arith_auto_config_simplex); //!< force simplex solver in auto_config
DISPLAY_PARAM(m_arith_blands_rule_threshold);

6
src/smt/params/theory_arith_params.h
View file

@ -20,7 +20,7 @@ Revision History:
#define THEORY_ARITH_PARAMS_H_
#include<limits.h>
#include"params.h"
#include "util/params.h"
enum arith_solver_id {
AS_NO_ARITH,
@ -49,6 +49,8 @@ enum arith_pivot_strategy {
};
struct theory_arith_params {
bool m_arith_eq2ineq;
bool m_arith_process_all_eqs;
arith_solver_id m_arith_mode;
bool m_arith_auto_config_simplex; //!< force simplex solver in auto_config
unsigned m_arith_blands_rule_threshold;
@ -108,6 +110,8 @@ struct theory_arith_params {
theory_arith_params(params_ref const & p = params_ref()):
m_arith_eq2ineq(false),
m_arith_process_all_eqs(false),
m_arith_mode(AS_ARITH),
m_arith_auto_config_simplex(false),
m_arith_blands_rule_threshold(1000),

4
src/smt/params/theory_array_params.cpp
View file

@ -16,8 +16,8 @@ Author:
Revision History:
--*/
#include"theory_array_params.h"
#include"smt_params_helper.hpp"
#include "smt/params/theory_array_params.h"
#include "smt/params/smt_params_helper.hpp"
void theory_array_params::updt_params(params_ref const & _p) {
smt_params_helper p(_p);

8
src/smt/params/theory_array_params.h
View file

@ -19,7 +19,7 @@ Revision History:
#ifndef THEORY_ARRAY_PARAMS_H_
#define THEORY_ARRAY_PARAMS_H_
#include"array_simplifier_params.h"
#include "util/params.h"
enum array_solver_id {
AR_NO_ARRAY,
@ -28,7 +28,9 @@ enum array_solver_id {
AR_FULL
};
struct theory_array_params : public array_simplifier_params {
struct theory_array_params {
bool m_array_canonize_simplify;
bool m_array_simplify; // temporary hack for disabling array simplifier plugin.
array_solver_id m_array_mode;
bool m_array_weak;
bool m_array_extensional;
@ -40,6 +42,8 @@ struct theory_array_params : public array_simplifier_params {
unsigned m_array_lazy_ieq_delay;
theory_array_params():
m_array_canonize_simplify(false),
m_array_simplify(true),
m_array_mode(AR_FULL),
m_array_weak(false),
m_array_extensional(true),

10
src/smt/params/theory_bv_params.cpp
View file

@ -16,11 +16,14 @@ Author:
Revision History:
--*/
#include"theory_bv_params.h"
#include"smt_params_helper.hpp"
#include "smt/params/theory_bv_params.h"
#include "smt/params/smt_params_helper.hpp"
#include "ast/rewriter/bv_rewriter_params.hpp"
void theory_bv_params::updt_params(params_ref const & _p) {
smt_params_helper p(_p);
bv_rewriter_params rp(_p);
m_hi_div0 = rp.hi_div0();
m_bv_reflect = p.bv_reflect();
m_bv_enable_int2bv2int = p.bv_enable_int2bv();
}
@ -29,9 +32,10 @@ void theory_bv_params::updt_params(params_ref const & _p) {
void theory_bv_params::display(std::ostream & out) const {
DISPLAY_PARAM(m_bv_mode);
DISPLAY_PARAM(m_hi_div0);
DISPLAY_PARAM(m_bv_reflect);
DISPLAY_PARAM(m_bv_lazy_le);
DISPLAY_PARAM(m_bv_cc);
DISPLAY_PARAM(m_bv_blast_max_size);
DISPLAY_PARAM(m_bv_enable_int2bv2int);
}
}

4
src/smt/params/theory_bv_params.h
View file

@ -19,7 +19,7 @@ Revision History:
#ifndef THEORY_BV_PARAMS_H_
#define THEORY_BV_PARAMS_H_
#include"params.h"
#include "util/params.h"
enum bv_solver_id {
BS_NO_BV,
@ -28,6 +28,7 @@ enum bv_solver_id {
struct theory_bv_params {
bv_solver_id m_bv_mode;
bool m_hi_div0; //!< if true, uses the hardware interpretation for div0, mod0, ... if false, div0, mod0, ... are considered uninterpreted.
bool m_bv_reflect;
bool m_bv_lazy_le;
bool m_bv_cc;
@ -35,6 +36,7 @@ struct theory_bv_params {
bool m_bv_enable_int2bv2int;
theory_bv_params(params_ref const & p = params_ref()):
m_bv_mode(BS_BLASTER),
m_hi_div0(false),
m_bv_reflect(true),
m_bv_lazy_le(false),
m_bv_cc(false),

4
src/smt/params/theory_pb_params.cpp
View file

@ -16,8 +16,8 @@ Author:
Revision History:
--*/
#include"theory_pb_params.h"
#include"smt_params_helper.hpp"
#include "smt/params/theory_pb_params.h"
#include "smt/params/smt_params_helper.hpp"
void theory_pb_params::updt_params(params_ref const & _p) {
smt_params_helper p(_p);

2
src/smt/params/theory_pb_params.h
View file

@ -19,7 +19,7 @@ Revision History:
#ifndef THEORY_PB_PARAMS_H_
#define THEORY_PB_PARAMS_H_
#include"params.h"
#include "util/params.h"
struct theory_pb_params {

4
src/smt/params/theory_str_params.cpp
View file

@ -15,8 +15,8 @@ Revision History:
--*/
#include"theory_str_params.h"
#include"smt_params_helper.hpp"
#include "smt/params/theory_str_params.h"
#include "smt/params/smt_params_helper.hpp"
void theory_str_params::updt_params(params_ref const & _p) {
smt_params_helper p(_p);

2
src/smt/params/theory_str_params.h
View file

@ -18,7 +18,7 @@ Revision History:
#ifndef THEORY_STR_PARAMS_H
#define THEORY_STR_PARAMS_H
#include"params.h"
#include "util/params.h"
struct theory_str_params {
/*

2
src/smt/proto_model/CMakeLists.txt
View file

@ -8,6 +8,6 @@ z3_add_component(proto_model
value_factory.cpp
COMPONENT_DEPENDENCIES
model
simplifier
rewriter
smt_params
)

10
src/smt/proto_model/array_factory.cpp
View file

@ -17,11 +17,11 @@ Revision History:
--*/
#include"array_factory.h"
#include"array_decl_plugin.h"
#include"proto_model.h"
#include"func_interp.h"
#include"ast_pp.h"
#include "smt/proto_model/array_factory.h"
#include "ast/array_decl_plugin.h"
#include "smt/proto_model/proto_model.h"
#include "model/func_interp.h"
#include "ast/ast_pp.h"
func_decl * mk_aux_decl_for_array_sort(ast_manager & m, sort * s) {
ptr_buffer<sort> domain;

2
src/smt/proto_model/array_factory.h
View file

@ -19,7 +19,7 @@ Revision History:
#ifndef ARRAY_FACTORY_H_
#define ARRAY_FACTORY_H_
#include"struct_factory.h"
#include "smt/proto_model/struct_factory.h"
class func_interp;

58
src/smt/proto_model/datatype_factory.cpp
View file

@ -16,11 +16,10 @@ Author:
Revision History:
--*/
#include"datatype_factory.h"
#include"proto_model.h"
#include"ast_pp.h"
#include"ast_ll_pp.h"
#include"expr_functors.h"
#include "smt/proto_model/datatype_factory.h"
#include "smt/proto_model/proto_model.h"
#include "ast/ast_pp.h"
#include "ast/expr_functors.h"
datatype_factory::datatype_factory(ast_manager & m, proto_model & md):
struct_factory(m, m.mk_family_id("datatype"), md),
@ -39,7 +38,7 @@ expr * datatype_factory::get_some_value(sort * s) {
}
expr * r = m_manager.mk_app(c, args.size(), args.c_ptr());
register_value(r);
TRACE("datatype_factory", tout << mk_pp(r, m_util.get_manager()) << "\n";);
TRACE("datatype", tout << mk_pp(r, m_util.get_manager()) << "\n";);
return r;
}
@ -49,7 +48,7 @@ expr * datatype_factory::get_some_value(sort * s) {
expr * datatype_factory::get_last_fresh_value(sort * s) {
expr * val = 0;
if (m_last_fresh_value.find(s, val)) {
TRACE("datatype_factory", tout << "cached fresh value: " << mk_pp(val, m_manager) << "\n";);
TRACE("datatype", tout << "cached fresh value: " << mk_pp(val, m_manager) << "\n";);
return val;
}
value_set * set = get_value_set(s);
@ -69,7 +68,7 @@ bool datatype_factory::is_subterm_of_last_value(app* e) {
}
contains_app contains(m_manager, e);
bool result = contains(last);
TRACE("datatype_factory", tout << mk_pp(e, m_manager) << " in " << mk_pp(last, m_manager) << " " << result << "\n";);
TRACE("datatype", tout << mk_pp(e, m_manager) << " in " << mk_pp(last, m_manager) << " " << result << "\n";);
return result;
}
@ -89,11 +88,8 @@ expr * datatype_factory::get_almost_fresh_value(sort * s) {
// Traverse constructors, and try to invoke get_fresh_value of one of the arguments (if the argument is not a sibling datatype of s).
// If the argumet is a sibling datatype of s, then
// use get_last_fresh_value.
ptr_vector<func_decl> const * constructors = m_util.get_datatype_constructors(s);
ptr_vector<func_decl>::const_iterator it = constructors->begin();
ptr_vector<func_decl>::const_iterator end = constructors->end();
for (; it != end; ++it) {
func_decl * constructor = *it;
ptr_vector<func_decl> const & constructors = *m_util.get_datatype_constructors(s);
for (func_decl * constructor : constructors) {
expr_ref_vector args(m_manager);
bool found_fresh_arg = false;
bool recursive = false;
@ -130,7 +126,7 @@ expr * datatype_factory::get_almost_fresh_value(sort * s) {
m_last_fresh_value.insert(s, new_value);
}
}
TRACE("datatype_factory", tout << "almost fresh: " << mk_pp(new_value, m_manager) << "\n";);
TRACE("datatype", tout << "almost fresh: " << mk_pp(new_value, m_manager) << "\n";);
return new_value;
}
}
@ -140,7 +136,7 @@ expr * datatype_factory::get_almost_fresh_value(sort * s) {
expr * datatype_factory::get_fresh_value(sort * s) {
TRACE("datatype_factory", tout << "generating fresh value for: " << s->get_name() << "\n";);
TRACE("datatype", tout << "generating fresh value for: " << s->get_name() << "\n";);
value_set * set = get_value_set(s);
// Approach 0)
// if no value for s was generated so far, then used get_some_value
@ -148,18 +144,15 @@ expr * datatype_factory::get_fresh_value(sort * s) {
expr * val = get_some_value(s);
if (m_util.is_recursive(s))
m_last_fresh_value.insert(s, val);
TRACE("datatype_factory", tout << "0. result: " << mk_pp(val, m_manager) << "\n";);
TRACE("datatype", tout << "0. result: " << mk_pp(val, m_manager) << "\n";);
return val;
}
// Approach 1)
// Traverse constructors, and try to invoke get_fresh_value of one of the
// arguments (if the argument is not a sibling datatype of s).
// Two datatypes are siblings if they were defined together in the same mutually recursive definition.
ptr_vector<func_decl> const * constructors = m_util.get_datatype_constructors(s);
ptr_vector<func_decl>::const_iterator it = constructors->begin();
ptr_vector<func_decl>::const_iterator end = constructors->end();
for (; it != end; ++it) {
func_decl * constructor = *it;
ptr_vector<func_decl> const & constructors = *m_util.get_datatype_constructors(s);
for (func_decl * constructor : constructors) {
expr_ref_vector args(m_manager);
bool found_fresh_arg = false;
unsigned num = constructor->get_arity();
@ -178,13 +171,13 @@ expr * datatype_factory::get_fresh_value(sort * s) {
}
expr_ref new_value(m_manager);
new_value = m_manager.mk_app(constructor, args.size(), args.c_ptr());
CTRACE("datatype_factory", found_fresh_arg && set->contains(new_value), tout << mk_pp(new_value, m_manager) << "\n";);
CTRACE("datatype", found_fresh_arg && set->contains(new_value), tout << mk_pp(new_value, m_manager) << "\n";);
SASSERT(!found_fresh_arg || !set->contains(new_value));
if (!set->contains(new_value)) {
register_value(new_value);
if (m_util.is_recursive(s))
m_last_fresh_value.insert(s, new_value);
TRACE("datatype_factory", tout << "1. result: " << mk_pp(new_value, m_manager) << "\n";);
TRACE("datatype", tout << "1. result: " << mk_pp(new_value, m_manager) << "\n";);
return new_value;
}
}
@ -195,19 +188,16 @@ expr * datatype_factory::get_fresh_value(sort * s) {
if (m_util.is_recursive(s)) {
while(true) {
++num_iterations;
TRACE("datatype_factory", tout << mk_pp(get_last_fresh_value(s), m_manager) << "\n";);
ptr_vector<func_decl> const * constructors = m_util.get_datatype_constructors(s);
ptr_vector<func_decl>::const_iterator it = constructors->begin();
ptr_vector<func_decl>::const_iterator end = constructors->end();
for (; it != end; ++it) {
func_decl * constructor = *it;
TRACE("datatype", tout << mk_pp(get_last_fresh_value(s), m_manager) << "\n";);
ptr_vector<func_decl> const & constructors = *m_util.get_datatype_constructors(s);
for (func_decl * constructor : constructors) {
expr_ref_vector args(m_manager);
bool found_sibling = false;
unsigned num = constructor->get_arity();
TRACE("datatype_factory", tout << "checking constructor: " << constructor->get_name() << "\n";);
TRACE("datatype", tout << "checking constructor: " << constructor->get_name() << "\n";);
for (unsigned i = 0; i < num; i++) {
sort * s_arg = constructor->get_domain(i);
TRACE("datatype_factory", tout << mk_pp(s, m_manager) << " "
TRACE("datatype", tout << mk_pp(s, m_manager) << " "
<< mk_pp(s_arg, m_manager) << " are_siblings "
<< m_util.are_siblings(s, s_arg) << " is_datatype "
<< m_util.is_datatype(s_arg) << " found_sibling "
@ -222,7 +212,7 @@ expr * datatype_factory::get_fresh_value(sort * s) {
maybe_new_arg = get_fresh_value(s_arg);
}
if (!maybe_new_arg) {
TRACE("datatype_factory",
TRACE("datatype",
tout << "no argument found for " << mk_pp(s_arg, m_manager) << "\n";);
maybe_new_arg = m_model.get_some_value(s_arg);
found_sibling = false;
@ -239,11 +229,11 @@ expr * datatype_factory::get_fresh_value(sort * s) {
if (found_sibling) {
expr_ref new_value(m_manager);
new_value = m_manager.mk_app(constructor, args.size(), args.c_ptr());
TRACE("datatype_factory", tout << "potential new value: " << mk_pp(new_value, m_manager) << "\n";);
TRACE("datatype", tout << "potential new value: " << mk_pp(new_value, m_manager) << "\n";);
m_last_fresh_value.insert(s, new_value);
if (!set->contains(new_value)) {
register_value(new_value);
TRACE("datatype_factory", tout << "2. result: " << mk_pp(new_value, m_manager) << "\n";);
TRACE("datatype", tout << "2. result: " << mk_pp(new_value, m_manager) << "\n";);
return new_value;
}
}

4
src/smt/proto_model/datatype_factory.h
View file

@ -19,8 +19,8 @@ Revision History:
#ifndef DATATYPE_FACTORY_H_
#define DATATYPE_FACTORY_H_
#include"struct_factory.h"
#include"datatype_decl_plugin.h"
#include "smt/proto_model/struct_factory.h"
#include "ast/datatype_decl_plugin.h"
class datatype_factory : public struct_factory {
datatype_util m_util;

4
src/smt/proto_model/numeral_factory.cpp
View file

@ -16,8 +16,8 @@ Author:
Revision History:
--*/
#include"numeral_factory.h"
#include"ast_pp.h"
#include "smt/proto_model/numeral_factory.h"
#include "ast/ast_pp.h"
app * arith_factory::mk_value_core(rational const & val, sort * s) {
return m_util.mk_numeral(val, s);

6
src/smt/proto_model/numeral_factory.h
View file

@ -19,9 +19,9 @@ Revision History:
#ifndef NUMERAL_FACTORY_H_
#define NUMERAL_FACTORY_H_
#include"value_factory.h"
#include"arith_decl_plugin.h"
#include"bv_decl_plugin.h"
#include "smt/proto_model/value_factory.h"
#include "ast/arith_decl_plugin.h"
#include "ast/bv_decl_plugin.h"
class numeral_factory : public simple_factory<rational> {
public:

364
src/smt/proto_model/proto_model.cpp
View file

@ -10,41 +10,40 @@ Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2007-03-08.
Revision History:
--*/
#include"proto_model.h"
#include"model_params.hpp"
#include"ast_pp.h"
#include"ast_ll_pp.h"
#include"var_subst.h"
#include"array_decl_plugin.h"
#include"well_sorted.h"
#include"used_symbols.h"
#include"model_v2_pp.h"
#include "ast/ast_pp.h"
#include "ast/ast_ll_pp.h"
#include "ast/rewriter/var_subst.h"
#include "ast/well_sorted.h"
#include "ast/used_symbols.h"
#include "model/model_params.hpp"
#include "model/model_v2_pp.h"
#include "smt/proto_model/proto_model.h"
proto_model::proto_model(ast_manager & m, params_ref const & p):
model_core(m),
m_afid(m.mk_family_id(symbol("array"))),
m_eval(*this),
m_rewrite(m) {
register_factory(alloc(basic_factory, m));
m_user_sort_factory = alloc(user_sort_factory, m);
register_factory(m_user_sort_factory);
m_model_partial = model_params(p).partial();
}
void proto_model::register_aux_decl(func_decl * d, func_interp * fi) {
model_core::register_decl(d, fi);
m_aux_decls.insert(d);
}
void proto_model::register_aux_decl(func_decl * d) {
m_aux_decls.insert(d);
}
/**
\brief Set new_fi as the new interpretation for f.
If f_aux != 0, then assign the old interpretation of f to f_aux.
@ -84,21 +83,11 @@ expr * proto_model::mk_some_interp_for(func_decl * d) {
}
bool proto_model::is_select_of_model_value(expr* e) const {
return
is_app_of(e, m_afid, OP_SELECT) &&
is_as_array(to_app(e)->get_arg(0)) &&
has_interpretation(array_util(m_manager).get_as_array_func_decl(to_app(to_app(e)->get_arg(0))));
}
bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) {
m_eval.set_model_completion(model_completion);
m_eval.set_expand_array_equalities(false);
try {
m_eval(e, result);
#if 0
std::cout << mk_pp(e, m_manager) << "\n===>\n" << result << "\n";
#endif
return true;
}
catch (model_evaluator_exception & ex) {
@ -158,12 +147,11 @@ void proto_model::cleanup_func_interp(func_interp * fi, func_decl_set & found_au
app * t = to_app(a);
bool visited = true;
args.reset();
unsigned num_args = t->get_num_args();
for (unsigned i = 0; i < num_args; ++i) {
for (expr* t_arg : *t) {
expr * arg = 0;
if (!cache.find(t->get_arg(i), arg)) {
if (!cache.find(t_arg, arg)) {
visited = false;
todo.push_back(t->get_arg(i));
todo.push_back(t_arg);
}
else {
args.push_back(arg);
@ -173,10 +161,12 @@ void proto_model::cleanup_func_interp(func_interp * fi, func_decl_set & found_au
continue;
}
func_decl * f = t->get_decl();
if (m_aux_decls.contains(f))
if (m_aux_decls.contains(f)) {
TRACE("model_bug", tout << f->get_name() << "\n";);
found_aux_fs.insert(f);
}
expr_ref new_t(m_manager);
new_t = m_rewrite.mk_app(f, num_args, args.c_ptr());
new_t = m_rewrite.mk_app(f, args.size(), args.c_ptr());
if (t != new_t.get())
trail.push_back(new_t);
todo.pop_back();
@ -192,9 +182,7 @@ void proto_model::cleanup_func_interp(func_interp * fi, func_decl_set & found_au
}
}
if (!cache.find(fi_else, a)) {
UNREACHABLE();
}
VERIFY(cache.find(fi_else, a));
fi->set_else(a);
}
@ -219,11 +207,11 @@ void proto_model::remove_aux_decls_not_in_set(ptr_vector<func_decl> & decls, fun
by their interpretations.
*/
void proto_model::cleanup() {
TRACE("model_bug", model_v2_pp(tout, *this););
func_decl_set found_aux_fs;
decl2finterp::iterator it = m_finterp.begin();
decl2finterp::iterator end = m_finterp.end();
for (; it != end; ++it) {
func_interp * fi = (*it).m_value;
for (auto const& kv : m_finterp) {
TRACE("model_bug", tout << kv.m_key->get_name() << "\n";);
func_interp * fi = kv.m_value;
cleanup_func_interp(fi, found_aux_fs);
}
@ -232,18 +220,10 @@ void proto_model::cleanup() {
remove_aux_decls_not_in_set(m_decls, found_aux_fs);
remove_aux_decls_not_in_set(m_func_decls, found_aux_fs);
func_decl_set::iterator it2 = m_aux_decls.begin();
func_decl_set::iterator end2 = m_aux_decls.end();
for (; it2 != end2; ++it2) {
func_decl * faux = *it2;
for (func_decl* faux : m_aux_decls) {
if (!found_aux_fs.contains(faux)) {
TRACE("cleanup_bug", tout << "eliminating " << faux->get_name() << "\n";);
func_interp * fi = 0;
m_finterp.find(faux, fi);
SASSERT(fi != 0);
m_finterp.erase(faux);
m_manager.dec_ref(faux);
dealloc(fi);
unregister_decl(faux);
}
}
m_aux_decls.swap(found_aux_fs);
@ -270,10 +250,9 @@ ptr_vector<expr> const & proto_model::get_universe(sort * s) const {
ptr_vector<expr> & tmp = const_cast<proto_model*>(this)->m_tmp;
tmp.reset();
obj_hashtable<expr> const & u = get_known_universe(s);
obj_hashtable<expr>::iterator it = u.begin();
obj_hashtable<expr>::iterator end = u.end();
for (; it != end; ++it)
tmp.push_back(*it);
for (expr * e : u) {
tmp.push_back(e);
}
return tmp;
}
@ -351,15 +330,8 @@ void proto_model::register_value(expr * n) {
}
}
bool proto_model::is_as_array(expr * v) const {
return is_app_of(v, m_afid, OP_AS_ARRAY);
}
void proto_model::compress() {
ptr_vector<func_decl>::iterator it = m_func_decls.begin();
ptr_vector<func_decl>::iterator end = m_func_decls.end();
for (; it != end; ++it) {
func_decl * f = *it;
for (func_decl* f : m_func_decls) {
func_interp * fi = get_func_interp(f);
SASSERT(fi != 0);
fi->compress();
@ -373,23 +345,9 @@ void proto_model::compress() {
void proto_model::complete_partial_func(func_decl * f) {
func_interp * fi = get_func_interp(f);
if (fi && fi->is_partial()) {
expr * else_value = 0;
#if 0
// For UFBV benchmarks, setting the "else" to false is not a good idea.
// TODO: find a permanent solution. A possibility is to add another option.
if (m_manager.is_bool(f->get_range())) {
else_value = m_manager.mk_false();
}
else {
else_value = fi->get_max_occ_result();
if (else_value == 0)
else_value = get_some_value(f->get_range());
}
#else
else_value = fi->get_max_occ_result();
expr * else_value = fi->get_max_occ_result();
if (else_value == 0)
else_value = get_some_value(f->get_range());
#endif
fi->set_else(else_value);
}
}
@ -409,20 +367,16 @@ void proto_model::complete_partial_funcs() {
}
model * proto_model::mk_model() {
TRACE("proto_model", tout << "mk_model\n"; model_v2_pp(tout, *this););
TRACE("proto_model", model_v2_pp(tout << "mk_model\n", *this););
model * m = alloc(model, m_manager);
decl2expr::iterator it1 = m_interp.begin();
decl2expr::iterator end1 = m_interp.end();
for (; it1 != end1; ++it1) {
m->register_decl(it1->m_key, it1->m_value);
for (auto const& kv : m_interp) {
m->register_decl(kv.m_key, kv.m_value);
}
decl2finterp::iterator it2 = m_finterp.begin();
decl2finterp::iterator end2 = m_finterp.end();
for (; it2 != end2; ++it2) {
m->register_decl(it2->m_key, it2->m_value);
m_manager.dec_ref(it2->m_key);
for (auto const& kv : m_finterp) {
m->register_decl(kv.m_key, kv.m_value);
m_manager.dec_ref(kv.m_key);
}
m_finterp.reset(); // m took the ownership of the func_interp's
@ -437,245 +391,3 @@ model * proto_model::mk_model() {
return m;
}
#if 0
#include"simplifier.h"
#include"basic_simplifier_plugin.h"
// Auxiliary function for computing fi(args[0], ..., args[fi.get_arity() - 1]).
// The result is stored in result.
// Return true if succeeded, and false otherwise.
// It uses the simplifier s during the computation.
bool eval(func_interp & fi, simplifier & s, expr * const * args, expr_ref & result) {
bool actuals_are_values = true;
if (fi.num_entries() != 0) {
for (unsigned i = 0; actuals_are_values && i < fi.get_arity(); i++) {
actuals_are_values = fi.m().is_value(args[i]);
}
}
func_entry * entry = fi.get_entry(args);
if (entry != 0) {
result = entry->get_result();
return true;
}
TRACE("func_interp", tout << "failed to find entry for: ";
for(unsigned i = 0; i < fi.get_arity(); i++)
tout << mk_pp(args[i], fi.m()) << " ";
tout << "\nis partial: " << fi.is_partial() << "\n";);
if (!fi.eval_else(args, result)) {
return false;
}
if (actuals_are_values && fi.args_are_values()) {
// cheap case... we are done
return true;
}
// build symbolic result... the actuals may be equal to the args of one of the entries.
basic_simplifier_plugin * bs = static_cast<basic_simplifier_plugin*>(s.get_plugin(fi.m().get_basic_family_id()));
for (unsigned k = 0; k < fi.num_entries(); k++) {
func_entry const * curr = fi.get_entry(k);
SASSERT(!curr->eq_args(fi.m(), fi.get_arity(), args));
if (!actuals_are_values || !curr->args_are_values()) {
expr_ref_buffer eqs(fi.m());
unsigned i = fi.get_arity();
while (i > 0) {
--i;
expr_ref new_eq(fi.m());
bs->mk_eq(curr->get_arg(i), args[i], new_eq);
eqs.push_back(new_eq);
}
SASSERT(eqs.size() == fi.get_arity());
expr_ref new_cond(fi.m());
bs->mk_and(eqs.size(), eqs.c_ptr(), new_cond);
bs->mk_ite(new_cond, curr->get_result(), result, result);
}
}
return true;
}
bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) {
bool is_ok = true;
SASSERT(is_well_sorted(m_manager, e));
TRACE("model_eval", tout << mk_pp(e, m_manager) << "\n";
tout << "sort: " << mk_pp(m_manager.get_sort(e), m_manager) << "\n";);
obj_map<expr, expr*> eval_cache;
expr_ref_vector trail(m_manager);
sbuffer<std::pair<expr*, expr*>, 128> todo;
ptr_buffer<expr> args;
expr * null = static_cast<expr*>(0);
todo.push_back(std::make_pair(e, null));
simplifier m_simplifier(m_manager);
expr * a;
expr * expanded_a;
while (!todo.empty()) {
std::pair<expr *, expr *> & p = todo.back();
a = p.first;
expanded_a = p.second;
if (expanded_a != 0) {
expr * r = 0;
eval_cache.find(expanded_a, r);
SASSERT(r != 0);
todo.pop_back();
eval_cache.insert(a, r);
TRACE("model_eval",
tout << "orig:\n" << mk_pp(a, m_manager) << "\n";
tout << "after beta reduction:\n" << mk_pp(expanded_a, m_manager) << "\n";
tout << "new:\n" << mk_pp(r, m_manager) << "\n";);
}
else {
switch(a->get_kind()) {
case AST_APP: {
app * t = to_app(a);
bool visited = true;
args.reset();
unsigned num_args = t->get_num_args();
for (unsigned i = 0; i < num_args; ++i) {
expr * arg = 0;
if (!eval_cache.find(t->get_arg(i), arg)) {
visited = false;
todo.push_back(std::make_pair(t->get_arg(i), null));
}
else {
args.push_back(arg);
}
}
if (!visited) {
continue;
}
SASSERT(args.size() == t->get_num_args());
expr_ref new_t(m_manager);
func_decl * f = t->get_decl();
if (!has_interpretation(f)) {
// the model does not assign an interpretation to f.
SASSERT(new_t.get() == 0);
if (f->get_family_id() == null_family_id) {
if (model_completion) {
// create an interpretation for f.
new_t = mk_some_interp_for(f);
}
else {
TRACE("model_eval", tout << f->get_name() << " is uninterpreted\n";);
is_ok = false;
}
}
if (new_t.get() == 0) {
// t is interpreted or model completion is disabled.
m_simplifier.mk_app(f, num_args, args.c_ptr(), new_t);
TRACE("model_eval", tout << mk_pp(t, m_manager) << " -> " << new_t << "\n";);
trail.push_back(new_t);
if (!is_app(new_t) || to_app(new_t)->get_decl() != f || is_select_of_model_value(new_t)) {
// if the result is not of the form (f ...), then assume we must simplify it.
expr * new_new_t = 0;
if (!eval_cache.find(new_t.get(), new_new_t)) {
todo.back().second = new_t;
todo.push_back(std::make_pair(new_t, null));
continue;
}
else {
new_t = new_new_t;
}
}
}
}
else {
// the model has an interpretaion for f.
if (num_args == 0) {
// t is a constant
new_t = get_const_interp(f);
}
else {
// t is a function application
SASSERT(new_t.get() == 0);
// try to use function graph first
func_interp * fi = get_func_interp(f);
SASSERT(fi->get_arity() == num_args);
expr_ref r1(m_manager);
// fi may be partial...
if (!::eval(*fi, m_simplifier, args.c_ptr(), r1)) {
SASSERT(fi->is_partial()); // fi->eval only fails when fi is partial.
if (model_completion) {
expr * r = get_some_value(f->get_range());
fi->set_else(r);
SASSERT(!fi->is_partial());
new_t = r;
}
else {
// f is an uninterpreted function, there is no need to use m_simplifier.mk_app
new_t = m_manager.mk_app(f, num_args, args.c_ptr());
trail.push_back(new_t);
TRACE("model_eval", tout << f->get_name() << " is uninterpreted\n";);
is_ok = false;
}
}
else {
SASSERT(r1);
trail.push_back(r1);
TRACE("model_eval", tout << mk_pp(a, m_manager) << "\nevaluates to: " << r1 << "\n";);
expr * r2 = 0;
if (!eval_cache.find(r1.get(), r2)) {
todo.back().second = r1;
todo.push_back(std::make_pair(r1, null));
continue;
}
else {
new_t = r2;
}
}
}
}
TRACE("model_eval",
tout << "orig:\n" << mk_pp(t, m_manager) << "\n";
tout << "new:\n" << mk_pp(new_t, m_manager) << "\n";);
todo.pop_back();
SASSERT(new_t.get() != 0);
eval_cache.insert(t, new_t);
break;
}
case AST_VAR:
SASSERT(a != 0);
eval_cache.insert(a, a);
todo.pop_back();
break;
case AST_QUANTIFIER:
TRACE("model_eval", tout << "found quantifier\n" << mk_pp(a, m_manager) << "\n";);
is_ok = false; // evaluator does not handle quantifiers.
SASSERT(a != 0);
eval_cache.insert(a, a);
todo.pop_back();
break;
default:
UNREACHABLE();
break;
}
}
}
if (!eval_cache.find(e, a)) {
TRACE("model_eval", tout << "FAILED e: " << mk_bounded_pp(e, m_manager) << "\n";);
UNREACHABLE();
}
result = a;
std::cout << mk_pp(e, m_manager) << "\n===>\n" << result << "\n";
TRACE("model_eval",
ast_ll_pp(tout << "original: ", m_manager, e);
ast_ll_pp(tout << "evaluated: ", m_manager, a);
ast_ll_pp(tout << "reduced: ", m_manager, result.get());
tout << "sort: " << mk_pp(m_manager.get_sort(e), m_manager) << "\n";
);
SASSERT(is_well_sorted(m_manager, result.get()));
return is_ok;
}
#endif

22
src/smt/proto_model/proto_model.h
View file

@ -28,20 +28,19 @@ Revision History:
#ifndef PROTO_MODEL_H_
#define PROTO_MODEL_H_
#include"model_core.h"
#include"model_evaluator.h"
#include"value_factory.h"
#include"plugin_manager.h"
#include"arith_decl_plugin.h"
#include"func_decl_dependencies.h"
#include"model.h"
#include"params.h"
#include"th_rewriter.h"
#include "model/model_core.h"
#include "model/model_evaluator.h"
#include "smt/proto_model/value_factory.h"
#include "util/plugin_manager.h"
#include "ast/arith_decl_plugin.h"
#include "ast/func_decl_dependencies.h"
#include "model/model.h"
#include "util/params.h"
#include "ast/rewriter/th_rewriter.h"
class proto_model : public model_core {
plugin_manager<value_factory> m_factories;
user_sort_factory * m_user_sort_factory;
family_id m_afid; //!< array family id: hack for displaying models in V1.x style
func_decl_set m_aux_decls;
ptr_vector<expr> m_tmp;
model_evaluator m_eval;
@ -58,7 +57,6 @@ class proto_model : public model_core {
void remove_aux_decls_not_in_set(ptr_vector<func_decl> & decls, func_decl_set const & s);
void cleanup_func_interp(func_interp * fi, func_decl_set & found_aux_fs);
bool is_select_of_model_value(expr* e) const;
public:
proto_model(ast_manager & m, params_ref const & p = params_ref());
@ -68,7 +66,6 @@ public:
bool eval(expr * e, expr_ref & result, bool model_completion = false);
bool is_as_array(expr * v) const;
value_factory * get_factory(family_id fid);
@ -84,6 +81,7 @@ public:
// Primitives for building models
//
void register_aux_decl(func_decl * f, func_interp * fi);
void register_aux_decl(func_decl * f);
void reregister_decl(func_decl * f, func_interp * new_fi, func_decl * f_aux);
void compress();
void cleanup();

4
src/smt/proto_model/struct_factory.cpp
View file

@ -16,8 +16,8 @@ Author:
Revision History:
--*/
#include"struct_factory.h"
#include"proto_model.h"
#include "smt/proto_model/struct_factory.h"
#include "smt/proto_model/proto_model.h"
struct_factory::value_set * struct_factory::get_value_set(sort * s) {
value_set * set = 0;

4
src/smt/proto_model/struct_factory.h
View file

@ -19,8 +19,8 @@ Revision History:
#ifndef STRUCT_FACTORY_H_
#define STRUCT_FACTORY_H_
#include"value_factory.h"
#include"obj_hashtable.h"
#include "smt/proto_model/value_factory.h"
#include "util/obj_hashtable.h"
class proto_model;

2
src/smt/proto_model/value_factory.cpp
View file

@ -17,7 +17,7 @@ Revision History:
--*/
#include"value_factory.h"
#include "smt/proto_model/value_factory.h"
value_factory::value_factory(ast_manager & m, family_id fid):
m_manager(m),

4
src/smt/proto_model/value_factory.h
View file

@ -19,8 +19,8 @@ Revision History:
#ifndef VALUE_FACTORY_H_
#define VALUE_FACTORY_H_
#include"ast.h"
#include"obj_hashtable.h"
#include "ast/ast.h"
#include "util/obj_hashtable.h"
/**
\brief Auxiliary object used during model construction.

24
src/smt/qi_queue.cpp
View file

@ -16,13 +16,13 @@ Author:
Revision History:
--*/
#include"smt_context.h"
#include"qi_queue.h"
#include"warning.h"
#include"ast_pp.h"
#include"ast_ll_pp.h"
#include"var_subst.h"
#include"stats.h"
#include "smt/smt_context.h"
#include "smt/qi_queue.h"
#include "util/warning.h"
#include "ast/ast_pp.h"
#include "ast/ast_ll_pp.h"
#include "ast/rewriter/var_subst.h"
#include "util/stats.h"
namespace smt {
@ -148,11 +148,8 @@ namespace smt {
}
void qi_queue::instantiate() {
svector<entry>::iterator it = m_new_entries.begin();
svector<entry>::iterator end = m_new_entries.end();
unsigned since_last_check = 0;
for (; it != end; ++it) {
entry & curr = *it;
for (entry & curr : m_new_entries) {
fingerprint * f = curr.m_qb;
quantifier * qa = static_cast<quantifier*>(f->get_data());
@ -227,9 +224,8 @@ namespace smt {
TRACE("qi_queue_instance", tout << "new instance:\n" << mk_pp(instance, m_manager) << "\n";);
expr_ref s_instance(m_manager);
proof_ref pr(m_manager);
simplifier & simp = m_context.get_simplifier();
simp(instance, s_instance, pr);
TRACE("qi_queue_bug", tout << "new instance after simplification:\n" << mk_pp(s_instance, m_manager) << "\n";);
m_context.get_rewriter()(instance, s_instance, pr);
TRACE("qi_queue_bug", tout << "new instance after simplification:\n" << s_instance << "\n";);
if (m_manager.is_true(s_instance)) {
TRACE("checker", tout << "reduced to true, before:\n" << mk_ll_pp(instance, m_manager););

20
src/smt/qi_queue.h
View file

@ -19,16 +19,16 @@ Revision History:
#ifndef QI_QUEUE_H_
#define QI_QUEUE_H_
#include"ast.h"
#include"smt_quantifier_stat.h"
#include"smt_checker.h"
#include"smt_quantifier.h"
#include"qi_params.h"
#include"fingerprints.h"
#include"cost_parser.h"
#include"cost_evaluator.h"
#include"cached_var_subst.h"
#include"statistics.h"
#include "ast/ast.h"
#include "smt/smt_quantifier_stat.h"
#include "smt/smt_checker.h"
#include "smt/smt_quantifier.h"
#include "smt/params/qi_params.h"
#include "smt/fingerprints.h"
#include "parsers/util/cost_parser.h"
#include "smt/cost_evaluator.h"
#include "smt/cached_var_subst.h"
#include "util/statistics.h"
namespace smt {
class context;

6
src/smt/smt2_extra_cmds.cpp
View file

@ -16,9 +16,9 @@ Author:
Notes:
--*/
#include"cmd_context.h"
#include"smt2parser.h"
#include"smt2_extra_cmds.h"
#include "cmd_context/cmd_context.h"
#include "parsers/smt2/smt2parser.h"
#include "smt/smt2_extra_cmds.h"
class include_cmd : public cmd {
char const * m_filename;

2
src/smt/smt_almost_cg_table.cpp
View file

@ -17,7 +17,7 @@ Revision History:
--*/
#include"smt_almost_cg_table.h"
#include "smt/smt_almost_cg_table.h"
namespace smt {

4
src/smt/smt_almost_cg_table.h
View file

@ -19,8 +19,8 @@ Revision History:
#ifndef SMT_ALMOST_CG_TABLE_H_
#define SMT_ALMOST_CG_TABLE_H_
#include"smt_enode.h"
#include"map.h"
#include "smt/smt_enode.h"
#include "util/map.h"
namespace smt {

4
src/smt/smt_b_justification.h
View file

@ -19,8 +19,8 @@ Revision History:
#ifndef SMT_B_JUSTIFICATION_H_
#define SMT_B_JUSTIFICATION_H_
#include"smt_literal.h"
#include"smt_clause.h"
#include "smt/smt_literal.h"
#include "smt/smt_clause.h"
namespace smt {

2
src/smt/smt_bool_var_data.h
View file

@ -19,7 +19,7 @@ Revision History:
#ifndef SMT_BOOL_VAR_DATA_H_
#define SMT_BOOL_VAR_DATA_H_
#include"smt_b_justification.h"
#include "smt/smt_b_justification.h"
namespace smt {

37
src/smt/smt_case_split_queue.cpp
View file

@ -16,14 +16,14 @@ Author:
Revision History:
--*/
#include"smt_context.h"
#include"smt_case_split_queue.h"
#include"warning.h"
#include"stopwatch.h"
#include"for_each_expr.h"
#include"ast_pp.h"
#include"map.h"
#include"hashtable.h"
#include "smt/smt_context.h"
#include "smt/smt_case_split_queue.h"
#include "util/warning.h"
#include "util/stopwatch.h"
#include "ast/for_each_expr.h"
#include "ast/ast_pp.h"
#include "util/map.h"
#include "util/hashtable.h"
namespace smt {
@ -51,9 +51,9 @@ namespace smt {
if (!m_theory_var_priority.find(v2, p_v2)) {
p_v2 = 0.0;
}
// add clause activity
p_v1 += m_activity[v1];
p_v2 += m_activity[v2];
// add clause activity
p_v1 += m_activity[v1];
p_v2 += m_activity[v2];
return p_v1 > p_v2;
}
};
@ -82,6 +82,7 @@ namespace smt {
virtual void mk_var_eh(bool_var v) {
m_queue.reserve(v+1);
SASSERT(!m_queue.contains(v));
m_queue.insert(v);
}
@ -130,10 +131,7 @@ namespace smt {
virtual void display(std::ostream & out) {
bool first = true;
bool_var_act_queue::const_iterator it = m_queue.begin();
bool_var_act_queue::const_iterator end = m_queue.end();
for (; it != end ; ++it) {
unsigned v = *it;
for (unsigned v : m_queue) {
if (m_context.get_assignment(v) == l_undef) {
if (first) {
out << "remaining case-splits:\n";
@ -143,8 +141,7 @@ namespace smt {
}
}
if (!first)
out << "\n";
out << "\n";
}
virtual ~act_case_split_queue() {};
@ -166,11 +163,15 @@ namespace smt {
act_case_split_queue::activity_increased_eh(v);
if (m_queue.contains(v))
m_queue.decreased(v);
if (m_delayed_queue.contains(v))
m_delayed_queue.decreased(v);
}
virtual void mk_var_eh(bool_var v) {
m_queue.reserve(v+1);
m_delayed_queue.reserve(v+1);
SASSERT(!m_delayed_queue.contains(v));
SASSERT(!m_queue.contains(v));
if (m_context.is_searching())
m_delayed_queue.insert(v);
else
@ -1099,8 +1100,6 @@ namespace smt {
#endif
GOAL_STOP();
//std::cout << "goal set, time " << m_goal_time.get_seconds() << "\n";
}
void set_global_generation()

6
src/smt/smt_case_split_queue.h
View file

@ -19,9 +19,9 @@ Revision History:
#ifndef SMT_CASE_SPLIT_QUEUE_H_
#define SMT_CASE_SPLIT_QUEUE_H_
#include"smt_types.h"
#include"heap.h"
#include"smt_params.h"
#include "smt/smt_types.h"
#include "util/heap.h"
#include "smt/params/smt_params.h"
namespace smt {
class context;

6
src/smt/smt_cg_table.cpp
View file

@ -16,9 +16,9 @@ Author:
Revision History:
--*/
#include"smt_cg_table.h"
#include"ast_pp.h"
#include"ast_ll_pp.h"
#include "smt/smt_cg_table.h"
#include "ast/ast_pp.h"
#include "ast/ast_ll_pp.h"
namespace smt {

6
src/smt/smt_cg_table.h
View file

@ -19,9 +19,9 @@ Revision History:
#ifndef SMT_CG_TABLE_H_
#define SMT_CG_TABLE_H_
#include"smt_enode.h"
#include"hashtable.h"
#include"chashtable.h"
#include "smt/smt_enode.h"
#include "util/hashtable.h"
#include "util/chashtable.h"
namespace smt {

6
src/smt/smt_checker.cpp
View file

@ -16,9 +16,9 @@ Author:
Revision History:
--*/
#include"smt_context.h"
#include"smt_checker.h"
#include"ast_ll_pp.h"
#include "smt/smt_context.h"
#include "smt/smt_checker.h"
#include "ast/ast_ll_pp.h"
namespace smt {

4
src/smt/smt_checker.h
View file

@ -19,8 +19,8 @@ Revision History:
#ifndef SMT_CHECKER_H_
#define SMT_CHECKER_H_
#include"ast.h"
#include"obj_hashtable.h"
#include "ast/ast.h"
#include "util/obj_hashtable.h"
namespace smt {

6
src/smt/smt_clause.cpp
View file

@ -16,9 +16,9 @@ Author:
Revision History:
--*/
#include"smt_clause.h"
#include"smt_justification.h"
#include"ast_ll_pp.h"
#include "smt/smt_clause.h"
#include "smt/smt_justification.h"
#include "ast/ast_ll_pp.h"
namespace smt {
/**

10
src/smt/smt_clause.h
View file

@ -19,11 +19,11 @@ Revision History:
#ifndef SMT_CLAUSE_H_
#define SMT_CLAUSE_H_
#include"ast.h"
#include"smt_literal.h"
#include"tptr.h"
#include"obj_hashtable.h"
#include"smt_justification.h"
#include "ast/ast.h"
#include "smt/smt_literal.h"
#include "util/tptr.h"
#include "util/obj_hashtable.h"
#include "smt/smt_justification.h"
namespace smt {

24
src/smt/smt_conflict_resolution.cpp
View file

@ -16,10 +16,10 @@ Author:
Revision History:
--*/
#include"smt_context.h"
#include"smt_conflict_resolution.h"
#include"ast_pp.h"
#include"ast_ll_pp.h"
#include "smt/smt_context.h"
#include "smt/smt_conflict_resolution.h"
#include "ast/ast_pp.h"
#include "ast/ast_ll_pp.h"
namespace smt {
@ -348,10 +348,8 @@ namespace smt {
literal_vector & antecedents = m_tmp_literal_vector;
antecedents.reset();
justification2literals_core(js, antecedents);
literal_vector::iterator it = antecedents.begin();
literal_vector::iterator end = antecedents.end();
for(; it != end; ++it)
process_antecedent(*it, num_marks);
for (literal l : antecedents)
process_antecedent(l, num_marks);
}
/**
@ -517,11 +515,13 @@ namespace smt {
}
TRACE("conflict", tout << "processing consequent: "; m_ctx.display_literal_verbose(tout, consequent); tout << "\n";
tout << "num_marks: " << num_marks << ", js kind: " << js.get_kind() << "\n";);
tout << "num_marks: " << num_marks << ", js kind: " << js.get_kind() << " level: " << m_ctx.get_assign_level(consequent) << "\n";
);
SASSERT(js != null_b_justification);
switch (js.get_kind()) {
case b_justification::CLAUSE: {
clause * cls = js.get_clause();
TRACE("conflict", m_ctx.display_clause_detail(tout, cls););
if (cls->is_lemma())
cls->inc_clause_activity();
unsigned num_lits = cls->get_num_literals();
@ -566,7 +566,7 @@ namespace smt {
if (m_ctx.is_marked(l.var()))
break;
CTRACE("conflict", m_ctx.get_assign_level(l) != m_conflict_lvl && m_ctx.get_assign_level(l) != m_ctx.get_base_level(),
tout << "assign_level(l): " << m_ctx.get_assign_level(l) << ", conflict_lvl: " << m_conflict_lvl << ", l: "; m_ctx.display_literal(tout, l);
tout << "assign_level(l): " << m_ctx.get_assign_level(l) << ", conflict_lvl: " << m_conflict_lvl << ", l: "; m_ctx.display_literal_verbose(tout, l);
tout << "\n";);
SASSERT(m_ctx.get_assign_level(l) == m_conflict_lvl ||
// it may also be an (out-of-order) asserted literal
@ -810,8 +810,6 @@ namespace smt {
m_new_proofs.push_back(pr);
return pr;
}
if (m_manager.coarse_grain_proofs())
return pr;
TRACE("norm_eq_proof",
tout << "#" << n1->get_owner_id() << " = #" << n2->get_owner_id() << "\n";
tout << mk_ll_pp(pr, m_manager, true, false););
@ -1217,7 +1215,7 @@ namespace smt {
mk_proof(rhs, c, prs2);
while (!prs2.empty()) {
proof * pr = prs2.back();
if (m_manager.fine_grain_proofs()) {
if (m_manager.proofs_enabled()) {
pr = m_manager.mk_symmetry(pr);
m_new_proofs.push_back(pr);
prs1.push_back(pr);

22
src/smt/smt_conflict_resolution.h
View file

@ -19,17 +19,17 @@ Revision History:
#ifndef SMT_CONFLICT_RESOLUTION_H_
#define SMT_CONFLICT_RESOLUTION_H_
#include"smt_literal.h"
#include"smt_bool_var_data.h"
#include"smt_justification.h"
#include"smt_enode.h"
#include"dyn_ack.h"
#include"obj_pair_hashtable.h"
#include"smt_params.h"
#include"obj_pair_hashtable.h"
#include"map.h"
#include"watch_list.h"
#include"obj_pair_set.h"
#include "smt/smt_literal.h"
#include "smt/smt_bool_var_data.h"
#include "smt/smt_justification.h"
#include "smt/smt_enode.h"
#include "smt/dyn_ack.h"
#include "util/obj_pair_hashtable.h"
#include "smt/params/smt_params.h"
#include "util/obj_pair_hashtable.h"
#include "util/map.h"
#include "smt/watch_list.h"
#include "util/obj_pair_set.h"
typedef approx_set_tpl<unsigned, u2u, unsigned> level_approx_set;

13
src/smt/smt_consequences.cpp
View file

@ -16,12 +16,13 @@ Author:
Revision History:
--*/
#include "smt_context.h"
#include "ast_util.h"
#include "datatype_decl_plugin.h"
#include "model_pp.h"
#include "max_cliques.h"
#include "stopwatch.h"
#include "util/max_cliques.h"
#include "util/stopwatch.h"
#include "ast/ast_util.h"
#include "ast/ast_pp.h"
#include "ast/datatype_decl_plugin.h"
#include "model/model_pp.h"
#include "smt/smt_context.h"
namespace smt {

768
src/smt/smt_context.cpp
View file

File diff suppressed because it is too large Load diff

77
src/smt/smt_context.h
View file

@ -19,36 +19,36 @@ Revision History:
#ifndef SMT_CONTEXT_H_
#define SMT_CONTEXT_H_
#include"smt_clause.h"
#include"smt_setup.h"
#include"smt_enode.h"
#include"smt_cg_table.h"
#include"smt_b_justification.h"
#include"smt_eq_justification.h"
#include"smt_justification.h"
#include"smt_bool_var_data.h"
#include"smt_theory.h"
#include"smt_quantifier.h"
#include"smt_quantifier_stat.h"
#include"smt_statistics.h"
#include"smt_conflict_resolution.h"
#include"smt_relevancy.h"
#include"smt_case_split_queue.h"
#include"smt_almost_cg_table.h"
#include"smt_failure.h"
#include"asserted_formulas.h"
#include"smt_types.h"
#include"dyn_ack.h"
#include"ast_smt_pp.h"
#include"watch_list.h"
#include"trail.h"
#include"fingerprints.h"
#include"ref.h"
#include"proto_model.h"
#include"model.h"
#include"timer.h"
#include"statistics.h"
#include"progress_callback.h"
#include "smt/smt_clause.h"
#include "smt/smt_setup.h"
#include "smt/smt_enode.h"
#include "smt/smt_cg_table.h"
#include "smt/smt_b_justification.h"
#include "smt/smt_eq_justification.h"
#include "smt/smt_justification.h"
#include "smt/smt_bool_var_data.h"
#include "smt/smt_theory.h"
#include "smt/smt_quantifier.h"
#include "smt/smt_quantifier_stat.h"
#include "smt/smt_statistics.h"
#include "smt/smt_conflict_resolution.h"
#include "smt/smt_relevancy.h"
#include "smt/smt_case_split_queue.h"
#include "smt/smt_almost_cg_table.h"
#include "smt/smt_failure.h"
#include "smt/asserted_formulas.h"
#include "smt/smt_types.h"
#include "smt/dyn_ack.h"
#include "ast/ast_smt_pp.h"
#include "smt/watch_list.h"
#include "util/trail.h"
#include "smt/fingerprints.h"
#include "util/ref.h"
#include "smt/proto_model/proto_model.h"
#include "model/model.h"
#include "util/timer.h"
#include "util/statistics.h"
#include "solver/progress_callback.h"
// there is a significant space overhead with allocating 1000+ contexts in
// the case that each context only references a few expressions.
@ -209,7 +209,7 @@ namespace smt {
~scoped_mk_model() {
if (m_ctx.m_proto_model.get() != 0) {
m_ctx.m_model = m_ctx.m_proto_model->mk_model();
m_ctx.add_rec_funs_to_model();
m_ctx.add_rec_funs_to_model();
m_ctx.m_proto_model = 0; // proto_model is not needed anymore.
}
}
@ -245,8 +245,8 @@ namespace smt {
return m_manager;
}
simplifier & get_simplifier() {
return m_asserted_formulas.get_simplifier();
th_rewriter & get_rewriter() {
return m_asserted_formulas.get_rewriter();
}
smt_params & get_fparams() {
@ -257,7 +257,7 @@ namespace smt {
return m_params;
}
bool get_cancel_flag() { return !m_manager.limit().inc(); }
bool get_cancel_flag();
region & get_region() {
return m_region;
@ -1040,6 +1040,7 @@ namespace smt {
if (act > ACTIVITY_LIMIT)
rescale_bool_var_activity();
m_case_split_queue->activity_increased_eh(v);
TRACE("case_split", tout << "v" << v << " " << m_bvar_inc << " -> " << act << "\n";);
}
protected:
@ -1466,8 +1467,6 @@ namespace smt {
bool set_logic(symbol const& logic) { return m_setup.set_logic(logic); }
void register_plugin(simplifier_plugin * s);
void register_plugin(theory * th);
void assert_expr(expr * e);
@ -1539,9 +1538,9 @@ namespace smt {
proof * get_asserted_formula_proof(unsigned idx) const { return m_asserted_formulas.get_formula_proof(idx); }
expr * const * get_asserted_formulas() const { return m_asserted_formulas.get_formulas(); }
void get_asserted_formulas(ptr_vector<expr>& r) const { m_asserted_formulas.get_assertions(r); }
proof * const * get_asserted_formula_proofs() const { return m_asserted_formulas.get_formula_proofs(); }
//proof * const * get_asserted_formula_proofs() const { return m_asserted_formulas.get_formula_proofs(); }
void get_assumptions_core(ptr_vector<expr> & result);
@ -1567,7 +1566,7 @@ namespace smt {
func_decl * get_macro_func_decl(unsigned i) const { return m_asserted_formulas.get_macro_func_decl(i); }
func_decl * get_macro_interpretation(unsigned i, expr_ref & interp) const { return m_asserted_formulas.get_macro_interpretation(i, interp); }
quantifier * get_macro_quantifier(func_decl * f) const { return m_asserted_formulas.get_macro_quantifier(f); }
void insert_macro(func_decl * f, quantifier * m, proof * pr) { m_asserted_formulas.insert_macro(f, m, pr); }
void insert_macro(func_decl * f, quantifier * m, proof * pr, expr_dependency * dep) { m_asserted_formulas.insert_macro(f, m, pr, dep); }
};
};

8
src/smt/smt_context_inv.cpp
View file

@ -16,10 +16,10 @@ Author:
Revision History:
--*/
#include"smt_context.h"
#include"ast_pp.h"
#include"ast_ll_pp.h"
#include"ast_smt2_pp.h"
#include "smt/smt_context.h"
#include "ast/ast_pp.h"
#include "ast/ast_ll_pp.h"
#include "ast/ast_smt2_pp.h"
namespace smt {

10
src/smt/smt_context_pp.cpp
View file

@ -16,11 +16,11 @@ Author:
Revision History:
--*/
#include"smt_context.h"
#include"ast_ll_pp.h"
#include"ast_pp.h"
#include"ast_smt_pp.h"
#include"stats.h"
#include "smt/smt_context.h"
#include "ast/ast_ll_pp.h"
#include "ast/ast_pp.h"
#include "ast/ast_smt_pp.h"
#include "util/stats.h"
namespace smt {

4
src/smt/smt_context_stat.cpp
View file

@ -16,8 +16,8 @@ Author:
Revision History:
--*/
#include"smt_context.h"
#include"ast_pp.h"
#include "smt/smt_context.h"
#include "ast/ast_pp.h"
namespace smt {

4
src/smt/smt_enode.cpp
View file

@ -16,8 +16,8 @@ Author:
Revision History:
--*/
#include"smt_context.h"
#include"smt_enode.h"
#include "smt/smt_context.h"
#include "smt/smt_enode.h"
namespace smt {

18
src/smt/smt_enode.h
View file

@ -19,11 +19,11 @@ Revision History:
#ifndef SMT_ENODE_H_
#define SMT_ENODE_H_
#include"ast.h"
#include"smt_types.h"
#include"smt_eq_justification.h"
#include"smt_theory_var_list.h"
#include"approx_set.h"
#include "ast/ast.h"
#include "smt/smt_types.h"
#include "smt/smt_eq_justification.h"
#include "smt/smt_theory_var_list.h"
#include "util/approx_set.h"
namespace smt {
/**
@ -40,10 +40,10 @@ namespace smt {
/** \ brief Use sparse maps in SMT solver.
Define this to use hash maps rather than vectors over ast
nodes. This is useful in the case there are many solvers, each
referencing few nodes from a large ast manager. There is some
unknown performance penalty for this. */
Define this to use hash maps rather than vectors over ast
nodes. This is useful in the case there are many solvers, each
referencing few nodes from a large ast manager. There is some
unknown performance penalty for this. */
// #define SPARSE_MAP

4
src/smt/smt_eq_justification.h
View file

@ -19,8 +19,8 @@ Revision History:
#ifndef SMT_EQ_JUSTIFICATION_H_
#define SMT_EQ_JUSTIFICATION_H_
#include"smt_literal.h"
#include"tptr.h"
#include "smt/smt_literal.h"
#include "util/tptr.h"
namespace smt {

8
src/smt/smt_farkas_util.cpp
View file

@ -19,10 +19,10 @@ Revision History:
--*/
#include "smt_farkas_util.h"
#include "ast_pp.h"
#include "th_rewriter.h"
#include "bool_rewriter.h"
#include "smt/smt_farkas_util.h"
#include "ast/ast_pp.h"
#include "ast/rewriter/th_rewriter.h"
#include "ast/rewriter/bool_rewriter.h"
namespace smt {

2
src/smt/smt_farkas_util.h
View file

@ -22,7 +22,7 @@ Revision History:
#ifndef FARKAS_UTIL_H_
#define FARKAS_UTIL_H_
#include "arith_decl_plugin.h"
#include "ast/arith_decl_plugin.h"
namespace smt {

8
src/smt/smt_for_each_relevant_expr.cpp
View file

@ -16,10 +16,10 @@ Author:
Revision History:
--*/
#include"smt_context.h"
#include"smt_for_each_relevant_expr.h"
#include"ast_pp.h"
#include"ast_ll_pp.h"
#include "smt/smt_context.h"
#include "smt/smt_for_each_relevant_expr.h"
#include "ast/ast_pp.h"
#include "ast/ast_ll_pp.h"
namespace smt {

6
src/smt/smt_for_each_relevant_expr.h
View file

@ -19,9 +19,9 @@ Revision History:
#ifndef SMT_FOR_EACH_RELEVANT_EXPR_H_
#define SMT_FOR_EACH_RELEVANT_EXPR_H_
#include"ast.h"
#include"obj_hashtable.h"
#include"vector.h"
#include "ast/ast.h"
#include "util/obj_hashtable.h"
#include "util/vector.h"
namespace smt {

22
src/smt/smt_implied_equalities.cpp
View file

@ -19,16 +19,16 @@ Revision History:
--*/
#include "smt_implied_equalities.h"
#include "union_find.h"
#include "ast_pp.h"
#include "array_decl_plugin.h"
#include "uint_set.h"
#include "smt_value_sort.h"
#include "model_smt2_pp.h"
#include "stopwatch.h"
#include "model.h"
#include "solver.h"
#include "smt/smt_implied_equalities.h"
#include "util/union_find.h"
#include "ast/ast_pp.h"
#include "ast/array_decl_plugin.h"
#include "util/uint_set.h"
#include "smt/smt_value_sort.h"
#include "model/model_smt2_pp.h"
#include "util/stopwatch.h"
#include "model/model.h"
#include "solver/solver.h"
namespace smt {
@ -284,7 +284,7 @@ namespace smt {
}
lbool reduce_cond(model_ref& model, expr* e) {
expr* e1, *e2;
expr* e1 = 0, *e2 = 0;
if (m.is_eq(e, e1, e2) && m_array_util.is_as_array(e1) && m_array_util.is_as_array(e2)) {
if (e1 == e2) {
return l_true;

6
src/smt/smt_implied_equalities.h
View file

@ -23,9 +23,9 @@ Revision History:
#ifndef SMT_IMPLIED_EQUALITIES_H_
#define SMT_IMPLIED_EQUALITIES_H_
#include"smt_solver.h"
#include"lbool.h"
#include"ast.h"
#include "smt/smt_solver.h"
#include "util/lbool.h"
#include "ast/ast.h"
namespace smt {

34
src/smt/smt_internalizer.cpp
View file

@ -16,13 +16,13 @@ Author:
Revision History:
--*/
#include"smt_context.h"
#include"expr_stat.h"
#include"ast_pp.h"
#include"ast_ll_pp.h"
#include"ast_smt2_pp.h"
#include"smt_model_finder.h"
#include"for_each_expr.h"
#include "smt/smt_context.h"
#include "ast/expr_stat.h"
#include "ast/ast_pp.h"
#include "ast/ast_ll_pp.h"
#include "ast/ast_smt2_pp.h"
#include "smt/smt_model_finder.h"
#include "ast/for_each_expr.h"
namespace smt {
@ -198,19 +198,19 @@ namespace smt {
if (get_depth(n) > DEEP_EXPR_THRESHOLD) {
// if the expression is deep, then execute topological sort to avoid
// stack overflow.
// a caveat is that theory internalizers do rely on recursive descent so
// internalization over these follows top-down
TRACE("deep_internalize", tout << "expression is deep: #" << n->get_id() << "\n" << mk_ll_pp(n, m_manager););
svector<expr_bool_pair> sorted_exprs;
top_sort_expr(n, sorted_exprs);
TRACE("deep_internalize",
svector<expr_bool_pair>::const_iterator it = sorted_exprs.begin();
svector<expr_bool_pair>::const_iterator end = sorted_exprs.end();
for (; it != end; ++it) {
tout << "#" << it->first->get_id() << " " << it->second << "\n";
});
svector<expr_bool_pair>::const_iterator it = sorted_exprs.begin();
svector<expr_bool_pair>::const_iterator end = sorted_exprs.end();
for (; it != end; ++it)
internalize(it->first, it->second);
TRACE("deep_internalize", for (auto & kv : sorted_exprs) tout << "#" << kv.first->get_id() << " " << kv.second << "\n"; );
for (auto & kv : sorted_exprs) {
expr* e = kv.first;
if (!is_app(e) ||
to_app(e)->get_family_id() == null_family_id ||
to_app(e)->get_family_id() == m_manager.get_basic_family_id())
internalize(e, kv.second);
}
}
SASSERT(m_manager.is_bool(n));
if (is_gate(m_manager, n)) {

10
src/smt/smt_justification.cpp
View file

@ -16,10 +16,10 @@ Author:
Revision History:
--*/
#include"smt_context.h"
#include"smt_conflict_resolution.h"
#include"ast_pp.h"
#include"ast_ll_pp.h"
#include "smt/smt_context.h"
#include "smt/smt_conflict_resolution.h"
#include "ast/ast_pp.h"
#include "ast/ast_ll_pp.h"
namespace smt {
@ -129,7 +129,7 @@ namespace smt {
if (m_node1 != m_node1->get_root()) {
proof * pr = cr.get_proof(m_node1, m_node1->get_root());
if (pr && m.fine_grain_proofs())
if (pr && m.proofs_enabled())
pr = m.mk_symmetry(pr);
prs.push_back(pr);
if (!pr)

9
src/smt/smt_justification.h
View file

@ -19,10 +19,10 @@ Revision History:
#ifndef SMT_JUSTIFICATION_H_
#define SMT_JUSTIFICATION_H_
#include"ast.h"
#include"smt_types.h"
#include"smt_literal.h"
#include"smt_eq_justification.h"
#include "ast/ast.h"
#include "smt/smt_types.h"
#include "smt/smt_literal.h"
#include "smt/smt_eq_justification.h"
namespace smt {
@ -181,6 +181,7 @@ namespace smt {
enode * m_node2;
public:
eq_propagation_justification(enode * n1, enode * n2):m_node1(n1), m_node2(n2) {
SASSERT(n1 != n2);
}
virtual void get_antecedents(conflict_resolution & cr);

24
src/smt/smt_kernel.cpp
View file

@ -16,10 +16,10 @@ Author:
Revision History:
--*/
#include"smt_kernel.h"
#include"smt_context.h"
#include"ast_smt2_pp.h"
#include"smt_params_helper.hpp"
#include "smt/smt_kernel.h"
#include "smt/smt_context.h"
#include "ast/ast_smt2_pp.h"
#include "smt/params/smt_params_helper.hpp"
namespace smt {
@ -60,10 +60,10 @@ namespace smt {
// m_kernel.display(out); <<< for external users it is just junk
// TODO: it will be replaced with assertion_stack.display
unsigned num = m_kernel.get_num_asserted_formulas();
expr * const * fms = m_kernel.get_asserted_formulas();
out << "(kernel";
for (unsigned i = 0; i < num; i++) {
out << "\n " << mk_ismt2_pp(fms[i], m(), 2);
expr* f = m_kernel.get_asserted_formula(i);
out << "\n " << mk_ismt2_pp(f, m(), 2);
}
out << ")";
}
@ -81,8 +81,12 @@ namespace smt {
return m_kernel.get_num_asserted_formulas();
}
expr * const * get_formulas() const {
return m_kernel.get_asserted_formulas();
void get_formulas(ptr_vector<expr>& fmls) const {
m_kernel.get_asserted_formulas(fmls);
}
expr* get_formula(unsigned i) const {
return m_kernel.get_asserted_formula(i);
}
void push() {
@ -241,8 +245,8 @@ namespace smt {
return m_imp->size();
}
expr * const * kernel::get_formulas() const {
return m_imp->get_formulas();
expr* kernel::get_formula(unsigned i) const {
return m_imp->get_formula(i);
}

19
src/smt/smt_kernel.h
View file

@ -27,12 +27,12 @@ Revision History:
#ifndef SMT_KERNEL_H_
#define SMT_KERNEL_H_
#include"ast.h"
#include"params.h"
#include"model.h"
#include"lbool.h"
#include"statistics.h"
#include"smt_failure.h"
#include "ast/ast.h"
#include "util/params.h"
#include "model/model.h"
#include "util/lbool.h"
#include "util/statistics.h"
#include "smt/smt_failure.h"
struct smt_params;
class progress_callback;
@ -85,7 +85,12 @@ namespace smt {
/**
\brief Return the array of asserted formulas.
*/
expr * const * get_formulas() const;
void get_formulas(ptr_vector<expr>& r) const;
/**
\brief return the formula at index idx.
*/
expr* get_formula(unsigned idx) const;
/**
\brief Create a backtracking point (aka scope level).

6
src/smt/smt_literal.cpp
View file

@ -16,9 +16,9 @@ Author:
Revision History:
--*/
#include"smt_literal.h"
#include"ast_pp.h"
#include"ast_ll_pp.h"
#include "smt/smt_literal.h"
#include "ast/ast_pp.h"
#include "ast/ast_ll_pp.h"
namespace smt {

6
src/smt/smt_literal.h
View file

@ -19,9 +19,9 @@ Revision History:
#ifndef SMT_LITERAL_H_
#define SMT_LITERAL_H_
#include"ast.h"
#include"smt_types.h"
#include"approx_set.h"
#include "ast/ast.h"
#include "smt/smt_types.h"
#include "util/approx_set.h"
namespace smt {
/**

100
src/smt/smt_model_checker.cpp
View file

@ -17,16 +17,15 @@ Revision History:
--*/
#include"smt_model_checker.h"
#include"smt_context.h"
#include"smt_model_finder.h"
#include"pull_quant.h"
#include"for_each_expr.h"
#include"var_subst.h"
#include"ast_pp.h"
#include"ast_ll_pp.h"
#include"model_pp.h"
#include"ast_smt2_pp.h"
#include "ast/normal_forms/pull_quant.h"
#include "ast/for_each_expr.h"
#include "ast/rewriter/var_subst.h"
#include "ast/ast_pp.h"
#include "ast/ast_smt2_pp.h"
#include "smt/smt_model_checker.h"
#include "smt/smt_context.h"
#include "smt/smt_model_finder.h"
#include "model/model_pp.h"
namespace smt {
@ -40,7 +39,7 @@ namespace smt {
m_max_cexs(1),
m_iteration_idx(0),
m_curr_model(0),
m_new_instances_bindings(m) {
m_pinned_exprs(m) {
}
model_checker::~model_checker() {
@ -53,8 +52,8 @@ namespace smt {
}
void model_checker::set_qm(quantifier_manager & qm) {
SASSERT(m_qm == 0);
SASSERT(m_context == 0);
SASSERT(m_qm == 0);
SASSERT(m_context == 0);
m_qm = &qm;
m_context = &(m_qm->get_context());
}
@ -65,11 +64,9 @@ namespace smt {
expr * model_checker::get_term_from_ctx(expr * val) {
if (m_value2expr.empty()) {
// populate m_value2expr
obj_map<enode, app *>::iterator it = m_root2value->begin();
obj_map<enode, app *>::iterator end = m_root2value->end();
for (; it != end; ++it) {
enode * n = (*it).m_key;
expr * val = (*it).m_value;
for (auto const& kv : *m_root2value) {
enode * n = kv.m_key;
expr * val = kv.m_value;
n = n->get_eq_enode_with_min_gen();
m_value2expr.insert(val, n->get_owner());
}
@ -89,10 +86,7 @@ namespace smt {
void model_checker::restrict_to_universe(expr * sk, obj_hashtable<expr> const & universe) {
SASSERT(!universe.empty());
ptr_buffer<expr> eqs;
obj_hashtable<expr>::iterator it = universe.begin();
obj_hashtable<expr>::iterator end = universe.end();
for (; it != end; ++it) {
expr * e = *it;
for (expr * e : universe) {
eqs.push_back(m.mk_eq(sk, e));
}
expr_ref fml(m.mk_or(eqs.size(), eqs.c_ptr()), m);
@ -112,7 +106,7 @@ namespace smt {
if (!m_curr_model->eval(q->get_expr(), tmp, true)) {
return;
}
TRACE("model_checker", tout << "q after applying interpretation:\n" << mk_ismt2_pp(tmp, m) << "\n";);
TRACE("model_checker", tout << "q after applying interpretation:\n" << mk_ismt2_pp(tmp, m) << "\n";);
ptr_buffer<expr> subst_args;
unsigned num_decls = q->get_num_decls();
subst_args.resize(num_decls, 0);
@ -139,7 +133,7 @@ namespace smt {
bool model_checker::add_instance(quantifier * q, model * cex, expr_ref_vector & sks, bool use_inv) {
if (cex == 0) {
TRACE("model_checker", tout << "no model is available\n";);
return false;
return false;
}
unsigned num_decls = q->get_num_decls();
// Remark: sks were created for the flat version of q.
@ -187,21 +181,24 @@ namespace smt {
}
bindings.set(num_decls - i - 1, sk_value);
}
TRACE("model_checker", tout << q->get_qid() << " found (use_inv: " << use_inv << ") new instance: ";
for (unsigned i = 0; i < num_decls; i++) {
tout << mk_ismt2_pp(bindings[i].get(), m) << " ";
}
tout << "\n";);
max_generation = std::max(m_qm->get_generation(q), max_generation);
add_instance(q, bindings, max_generation);
return true;
}
void model_checker::add_instance(quantifier* q, expr_ref_vector const& bindings, unsigned max_generation) {
for (unsigned i = 0; i < bindings.size(); i++)
m_new_instances_bindings.push_back(bindings[i]);
SASSERT(q->get_num_decls() == bindings.size());
for (expr* b : bindings)
m_pinned_exprs.push_back(b);
m_pinned_exprs.push_back(q);
void * mem = m_new_instances_region.allocate(instance::get_obj_size(q->get_num_decls()));
instance * new_inst = new (mem) instance(q, bindings.c_ptr(), max_generation);
m_new_instances.push_back(new_inst);
@ -233,10 +230,8 @@ namespace smt {
bool model_checker::add_blocking_clause(model * cex, expr_ref_vector & sks) {
SASSERT(cex != 0);
unsigned num_sks = sks.size();
expr_ref_buffer diseqs(m);
for (unsigned i = 0; i < num_sks; i++) {
expr * sk = sks.get(i);
for (expr * sk : sks) {
func_decl * sk_d = to_app(sk)->get_decl();
expr_ref sk_value(m);
sk_value = cex->get_const_interp(sk_d);
@ -260,39 +255,38 @@ namespace smt {
bool model_checker::check(quantifier * q) {
SASSERT(!m_aux_context->relevancy());
m_aux_context->push();
quantifier * flat_q = get_flat_quantifier(q);
TRACE("model_checker", tout << "model checking:\n" << mk_ismt2_pp(q->get_expr(), m) << "\n" <<
TRACE("model_checker", tout << "model checking:\n" << mk_ismt2_pp(q->get_expr(), m) << "\n" <<
mk_ismt2_pp(flat_q->get_expr(), m) << "\n";);
expr_ref_vector sks(m);
assert_neg_q_m(flat_q, sks);
TRACE("model_checker", tout << "skolems:\n";
for (unsigned i = 0; i < sks.size(); i++) {
expr * sk = sks.get(i);
TRACE("model_checker", tout << "skolems:\n";
for (expr* sk : sks) {
tout << mk_ismt2_pp(sk, m) << " " << mk_pp(m.get_sort(sk), m) << "\n";
});
lbool r = m_aux_context->check();
TRACE("model_checker", tout << "[complete] model-checker result: " << to_sat_str(r) << "\n";);
if (r != l_true) {
m_aux_context->pop(1);
return r == l_false; // quantifier is satisfied by m_curr_model
}
model_ref complete_cex;
m_aux_context->get_model(complete_cex);
m_aux_context->get_model(complete_cex);
// try to find new instances using instantiation sets.
m_model_finder.restrict_sks_to_inst_set(m_aux_context.get(), q, sks);
unsigned num_new_instances = 0;
while (true) {
lbool r = m_aux_context->check();
TRACE("model_checker", tout << "[restricted] model-checker (" << (num_new_instances+1) << ") result: " << to_sat_str(r) << "\n";);
TRACE("model_checker", tout << "[restricted] model-checker (" << (num_new_instances+1) << ") result: " << to_sat_str(r) << "\n";);
if (r != l_true)
break;
break;
model_ref cex;
m_aux_context->get_model(cex);
if (!add_instance(q, cex.get(), sks, true)) {
@ -302,7 +296,7 @@ namespace smt {
if (num_new_instances >= m_max_cexs || !add_blocking_clause(cex.get(), sks)) {
TRACE("model_checker", tout << "Add blocking clause failed new-instances: " << num_new_instances << " max-cex: " << m_max_cexs << "\n";);
// add_blocking_clause failed... stop the search for new counter-examples...
break;
break;
}
}
@ -395,17 +389,17 @@ namespace smt {
check_quantifiers(false, found_relevant, num_failures);
if (found_relevant)
m_iteration_idx++;
TRACE("model_checker", tout << "model after check:\n"; model_pp(tout, *md););
TRACE("model_checker", tout << "model checker result: " << (num_failures == 0) << "\n";);
TRACE("model_checker", tout << "model checker result: " << (num_failures == 0) << "\n";);
m_max_cexs += m_params.m_mbqi_max_cexs;
if (num_failures == 0 && !m_context->validate_model()) {
num_failures = 1;
// this time force expanding recursive function definitions
// this time force expanding recursive function definitions
// that are not forced true in the current model.
check_quantifiers(true, found_relevant, num_failures);
}
@ -426,7 +420,7 @@ namespace smt {
for (; it != end; ++it) {
quantifier * q = *it;
if(!m_qm->mbqi_enabled(q)) continue;
TRACE("model_checker",
TRACE("model_checker",
tout << "Check: " << mk_pp(q, m) << "\n";
tout << m_context->get_assignment(q) << "\n";);
@ -469,8 +463,9 @@ namespace smt {
}
void model_checker::reset_new_instances() {
m_new_instances_region.reset();
m_pinned_exprs.reset();
m_new_instances.reset();
m_new_instances_region.reset();
}
void model_checker::reset() {
@ -481,10 +476,7 @@ namespace smt {
TRACE("model_checker_bug_detail", tout << "assert_new_instances, inconsistent: " << m_context->inconsistent() << "\n";);
ptr_buffer<enode> bindings;
ptr_vector<enode> dummy;
ptr_vector<instance>::iterator it = m_new_instances.begin();
ptr_vector<instance>::iterator end = m_new_instances.end();
for (; it != end; ++it) {
instance * inst = *it;
for (instance* inst : m_new_instances) {
quantifier * q = inst->m_q;
if (m_context->b_internalized(q)) {
bindings.reset();
@ -505,7 +497,7 @@ namespace smt {
expr * b = inst->m_bindings[i];
tout << mk_pp(b, m) << "\n";
});
TRACE("model_checker_instance",
TRACE("model_checker_instance",
expr_ref inst_expr(m);
instantiate(m, q, inst->m_bindings, inst_expr);
tout << "(assert " << mk_ismt2_pp(inst_expr, m) << ")\n";);

18
src/smt/smt_model_checker.h
View file

@ -21,11 +21,11 @@ Revision History:
#ifndef SMT_MODEL_CHECKER_H_
#define SMT_MODEL_CHECKER_H_
#include"ast.h"
#include"obj_hashtable.h"
#include"qi_params.h"
#include"smt_params.h"
#include"region.h"
#include "ast/ast.h"
#include "util/obj_hashtable.h"
#include "smt/params/qi_params.h"
#include "smt/params/smt_params.h"
#include "util/region.h"
class proto_model;
class model;
@ -39,7 +39,7 @@ namespace smt {
class model_checker {
ast_manager & m; // _manager;
qi_params const & m_params;
// copy of smt_params for auxiliary context.
// copy of smt_params for auxiliary context.
// the idea is to use a different configuration for the aux context (e.g., disable relevancy)
scoped_ptr<smt_params> m_fparams;
quantifier_manager * m_qm;
@ -73,8 +73,8 @@ namespace smt {
};
region m_new_instances_region;
expr_ref_vector m_new_instances_bindings;
ptr_vector<instance> m_new_instances;
expr_ref_vector m_pinned_exprs;
bool add_instance(quantifier * q, model * cex, expr_ref_vector & sks, bool use_inv);
void reset_new_instances();
void assert_new_instances();
@ -83,8 +83,8 @@ namespace smt {
struct is_model_value {};
expr_mark m_visited;
bool contains_model_value(expr* e);
void add_instance(quantifier* q, expr_ref_vector const& bindings, unsigned max_generation);
bool contains_model_value(expr * e);
void add_instance(quantifier * q, expr_ref_vector const & bindings, unsigned max_generation);
public:
model_checker(ast_manager & m, qi_params const & p, model_finder & mf);

1154
src/smt/smt_model_finder.cpp
View file

File diff suppressed because it is too large Load diff

Some files were not shown because too many files have changed in this diff Show more