mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

Merge branch 'unstable' of https://git01.codeplex.com/z3 into fpa-api

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2013-06-26 18:17:46 +01:00
parent de98426649 0d2a7f922c
commit b9aa721365
60 changed files with 1315 additions and 520 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

44
scripts/mk_util.py
View file

@ -1785,7 +1785,7 @@ def update_version():
raise MKException("set_version(major, minor, build, revision) must be used before invoking update_version()")
if not ONLY_MAKEFILES:
mk_version_dot_h(major, minor, build, revision)
update_all_assembly_infos(major, minor, build, revision)
mk_all_assembly_infos(major, minor, build, revision)
mk_def_files()
# Update files with the version number
@ -1800,49 +1800,32 @@ def mk_version_dot_h(major, minor, build, revision):
if VERBOSE:
print("Generated '%s'" % os.path.join(c.src_dir, 'version.h'))
# Update version number in AssemblyInfo.cs files
def update_all_assembly_infos(major, minor, build, revision):
# Generate AssemblyInfo.cs files with the right version numbers by using AssemblyInfo files as a template
def mk_all_assembly_infos(major, minor, build, revision):
for c in get_components():
if c.has_assembly_info():
assembly = os.path.join(c.src_dir, c.assembly_info_dir, 'AssemblyInfo.cs')
assembly = os.path.join(c.src_dir, c.assembly_info_dir, 'AssemblyInfo')
if os.path.exists(assembly):
# It is a CS file
update_assembly_info_version(assembly,
major, minor, build, revision, False)
mk_assembly_info_version(assembly, major, minor, build, revision)
else:
assembly = os.path.join(c.src_dir, c.assembly_info_dir, 'AssemblyInfo.cs')
if os.path.exists(assembly):
# It is a cpp file
update_assembly_info_version(assembly,
major, minor, build, revision, True)
else:
raise MKException("Failed to find assembly info file at '%s'" % os.path.join(c.src_dir, c.assembly_info_dir))
raise MKException("Failed to find assembly info file 'AssemblyInfo' at '%s'" % os.path.join(c.src_dir, c.assembly_info_dir))
# Update version number in the given AssemblyInfo.cs files
def update_assembly_info_version(assemblyinfo, major, minor, build, revision, is_cpp=False):
if is_cpp:
ver_pat = re.compile('[assembly:AssemblyVersionAttribute\("[\.\d]*"\) *')
fver_pat = re.compile('[assembly:AssemblyFileVersionAttribute\("[\.\d]*"\) *')
else:
ver_pat = re.compile('[assembly: AssemblyVersion\("[\.\d]*"\) *')
fver_pat = re.compile('[assembly: AssemblyFileVersion\("[\.\d]*"\) *')
# Generate version number in the given 'AssemblyInfo.cs' file using 'AssemblyInfo' as a template.
def mk_assembly_info_version(assemblyinfo, major, minor, build, revision):
ver_pat = re.compile('[assembly: AssemblyVersion\("[\.\d]*"\) *')
fver_pat = re.compile('[assembly: AssemblyFileVersion\("[\.\d]*"\) *')
fin = open(assemblyinfo, 'r')
tmp = '%s.new' % assemblyinfo
tmp = '%s.cs' % assemblyinfo
fout = open(tmp, 'w')
num_updates = 0
for line in fin:
if ver_pat.match(line):
if is_cpp:
fout.write('[assembly:AssemblyVersionAttribute("%s.%s.%s.%s")];\n' % (major, minor, build, revision))
else:
fout.write('[assembly: AssemblyVersion("%s.%s.%s.%s")]\n' % (major, minor, build, revision))
fout.write('[assembly: AssemblyVersion("%s.%s.%s.%s")]\n' % (major, minor, build, revision))
num_updates = num_updates + 1
elif fver_pat.match(line):
if is_cpp:
fout.write('[assembly:AssemblyFileVersionAttribute("%s.%s.%s.%s")];\n' % (major, minor, build, revision))
else:
fout.write('[assembly: AssemblyFileVersion("%s.%s.%s.%s")]\n' % (major, minor, build, revision))
fout.write('[assembly: AssemblyFileVersion("%s.%s.%s.%s")]\n' % (major, minor, build, revision))
num_updates = num_updates + 1
else:
fout.write(line)
@ -1851,7 +1834,6 @@ def update_assembly_info_version(assemblyinfo, major, minor, build, revision, is
assert num_updates == 2, "unexpected number of version number updates"
fin.close()
fout.close()
shutil.move(tmp, assemblyinfo)
if VERBOSE:
print("Updated '%s'" % assemblyinfo)

7
src/api/api_datalog.cpp
View file

@ -48,8 +48,11 @@ namespace api {
if (!m.has_plugin(name)) {
m.register_plugin(name, alloc(datalog::dl_decl_plugin));
}
datalog::relation_manager& r = m_context.get_rel_context().get_rmanager();
r.register_plugin(alloc(datalog::external_relation_plugin, *this, r));
datalog::rel_context* rel = m_context.get_rel_context();
if (rel) {
datalog::relation_manager& r = rel->get_rmanager();
r.register_plugin(alloc(datalog::external_relation_plugin, *this, r));
}
}
void fixedpoint_context::reduce(func_decl* f, unsigned num_args, expr * const* args, expr_ref& result) {

0
src/api/dotnet/Properties/AssemblyInfo.cs → src/api/dotnet/Properties/AssemblyInfo
View file

2
src/api/java/Status.java
View file

@ -12,7 +12,7 @@ package com.microsoft.z3;
public enum Status
{
// / Used to signify an unsatisfiable status.
UNSATISFIABLE(1),
UNSATISFIABLE(-1),
// / Used to signify an unknown status.
UNKNOWN(0),

6
src/api/z3_api.h
View file

@ -780,11 +780,11 @@ typedef enum
}
or
\nicebox{
(=> (and ln+1 ln+2 .. ln+m) l0)
(=> (and l1 l2 .. ln) l0)
}
or in the most general (ground) form:
\nicebox{
(=> (and ln+1 ln+2 .. ln+m) (or l0 l1 .. ln-1))
(=> (and ln+1 ln+2 .. ln+m) (or l0 l1 .. ln))
}
In other words we use the following (Prolog style) convention for Horn
implications:
@ -800,7 +800,7 @@ typedef enum
general non-ground form is:
\nicebox{
(forall (vars) (=> (and ln+1 ln+2 .. ln+m) (or l0 l1 .. ln-1)))
(forall (vars) (=> (and ln+1 ln+2 .. ln+m) (or l0 l1 .. ln)))
}
The hyper-resolution rule takes a sequence of parameters.

1
src/api/z3_replayer.cpp
View file

@ -26,6 +26,7 @@ Notes:
void register_z3_replayer_cmds(z3_replayer & in);
void throw_invalid_reference() {
TRACE("z3_replayer", tout << "invalid argument reference\n";);
throw z3_replayer_exception("invalid argument reference");
}

7
src/ast/rewriter/expr_safe_replace.cpp
View file

@ -106,3 +106,10 @@ void expr_safe_replace::reset() {
m_dst.reset();
m_subst.reset();
}
void expr_safe_replace::apply_substitution(expr* s, expr* def, expr_ref& t) {
reset();
insert(s, def);
(*this)(t, t);
reset();
}

2
src/ast/rewriter/expr_safe_replace.h
View file

@ -39,6 +39,8 @@ public:
void operator()(expr* src, expr_ref& e);
void apply_substitution(expr* s, expr* def, expr_ref& t);
void reset();
};

6
src/ast/rewriter/float_rewriter.cpp
View file

@ -88,7 +88,7 @@ br_status float_rewriter::mk_to_float(func_decl * f, unsigned num_args, expr * c
m_util.fm().set(v, ebits, sbits, rm, q.to_mpq());
result = m_util.mk_value(v);
m_util.fm().del(v);
TRACE("fp_rewriter", tout << "result: " << result << std::endl; );
// TRACE("fp_rewriter", tout << "result: " << result << std::endl; );
return BR_DONE;
}
else if (m_util.is_value(args[1], q_mpf)) {
@ -97,7 +97,7 @@ br_status float_rewriter::mk_to_float(func_decl * f, unsigned num_args, expr * c
m_util.fm().set(v, ebits, sbits, rm, q_mpf);
result = m_util.mk_value(v);
m_util.fm().del(v);
TRACE("fp_rewriter", tout << "result: " << result << std::endl; );
// TRACE("fp_rewriter", tout << "result: " << result << std::endl; );
return BR_DONE;
}
else
@ -125,7 +125,7 @@ br_status float_rewriter::mk_to_float(func_decl * f, unsigned num_args, expr * c
m_util.fm().set(v, ebits, sbits, rm, q.to_mpq(), e.to_mpq().numerator());
result = m_util.mk_value(v);
m_util.fm().del(v);
TRACE("fp_rewriter", tout << "result: " << result << std::endl; );
// TRACE("fp_rewriter", tout << "result: " << result << std::endl; );
return BR_DONE;
}
else {

1
src/muz_qe/clp_context.cpp
View file

@ -205,6 +205,7 @@ namespace datalog {
};
clp::clp(context& ctx):
engine_base(ctx.get_manager(), "clp"),
m_imp(alloc(imp, ctx)) {
}
clp::~clp() {

17
src/muz_qe/clp_context.h
View file

@ -22,23 +22,24 @@ Revision History:
#include "ast.h"
#include "lbool.h"
#include "statistics.h"
#include "dl_util.h"
namespace datalog {
class context;
class clp {
class clp : public datalog::engine_base {
class imp;
imp* m_imp;
public:
clp(context& ctx);
~clp();
lbool query(expr* query);
void cancel();
void cleanup();
void reset_statistics();
void collect_statistics(statistics& st) const;
void display_certificate(std::ostream& out) const;
expr_ref get_answer();
virtual lbool query(expr* query);
virtual void cancel();
virtual void cleanup();
virtual void reset_statistics();
virtual void collect_statistics(statistics& st) const;
virtual void display_certificate(std::ostream& out) const;
virtual expr_ref get_answer();
};
};

1
src/muz_qe/dl_bmc_engine.cpp
View file

@ -1416,6 +1416,7 @@ namespace datalog {
};
bmc::bmc(context& ctx):
engine_base(ctx.get_manager(), "bmc"),
m_ctx(ctx),
m(ctx.get_manager()),
m_solver(m, m_fparams),

2
src/muz_qe/dl_bmc_engine.h
View file

@ -30,7 +30,7 @@ Revision History:
namespace datalog {
class context;
class bmc {
class bmc : public engine_base {
context& m_ctx;
ast_manager& m;
smt_params m_fparams;

297
src/muz_qe/dl_boogie_proof.cpp Normal file
View file

@ -0,0 +1,297 @@
/**
Example from Boogie:
(derivation
(step s!4 (main_loop_LoopHead true true)
rule!3 (subst
(= assertsPassed@@1 true)
(= assertsPassed@2@@0 true)
(= main_loop_LoopHead_assertsPassed true)
)
(labels @950 +895 +668 +670 +893 +899 )
(ref true ))
(step s!3 (main true false)
rule!1 (subst
(= assertsPassed true)
(= assertsPassed@0 true)
(= assertsPassed@2 false)
(= main_assertsPassed false)
)
(labels @839 +763 +547 +546 +761 +544 +545 +si_fcall_805 +681 +768 )
(ref s!4 ))
(step s!2 (main_SeqInstr true false)
rule!2 (subst
(= assertsPassed@@0 true)
(= assertsPassed@0@@0 false)
(= main_SeqInstr_assertsPassed false)
)
(labels @890 +851 +572 +si_fcall_883 +853 )
(ref s!3 ))
(step s!1 (@Fail!0)
rule!4 (subst
(= assertsPassed@@2 true)
(= main_SeqInstr_assertsPassed@@0 false)
)
(labels )
(ref s!2 ))
)
(model
"tickleBool -> {
true -> true
false -> true
else -> true
}
")
*/
#include "dl_boogie_proof.h"
#include "model_pp.h"
#include "proof_utils.h"
#include "ast_pp.h"
#include "dl_util.h"
namespace datalog {
/**
\brief push hyper-resolution steps upwards such that every use of
hyper-resolution uses a premise that is not derived from hyper-resolution.
perform the following rewrite:
hr(hr(p1,p2,p3,..),p4,p5) => hr(p1,hr(p2,p4),p3,..,p5)
*/
void mk_input_resolution(proof_ref& pr) {
ast_manager& m = pr.get_manager();
proof_ref pr1(m);
proof_ref_vector premises1(m), premises2(m), premises(m);
expr_ref conclusion1(m), conclusion2(m), conclusion(m);
svector<std::pair<unsigned, unsigned> > positions1, positions2, positions;
vector<expr_ref_vector> substs1, substs2, substs;
if (m.is_hyper_resolve(pr, premises1, conclusion1, positions1, substs1) &&
m.is_hyper_resolve(premises1[0].get(), premises, conclusion2, positions, substs2)) {
for (unsigned i = 1; i < premises1.size(); ++i) {
pr1 = premises1[i].get();
mk_input_resolution(pr1);
premises1[i] = pr1;
}
for (unsigned i = 0; i < premises.size(); ++i) {
pr1 = premises[i].get();
mk_input_resolution(pr1);
premises[i] = pr1;
}
unsigned sz = premises.size();
for (unsigned i = 1; i < sz; ++i) {
proof* premise = premises[i].get();
expr_ref_vector literals(m);
expr* l1, *l2;
if (!m.is_implies(premise, l1, l2)) {
continue;
}
datalog::flatten_and(l1, literals);
positions2.reset();
premises2.reset();
premises2.push_back(premise);
substs2.reset();
for (unsigned j = 0; j < literals.size(); ++j) {
expr* lit = literals[j].get();
for (unsigned k = 1; k < premises1.size(); ++k) {
if (m.get_fact(premises1[k].get()) == lit) {
premises2.push_back(premises1[k].get());
positions2.push_back(std::make_pair(j+1,0));
substs2.push_back(expr_ref_vector(m));
break;
}
}
}
premises[i] = m.mk_hyper_resolve(premises2.size(), premises2.c_ptr(), l2, positions2, substs2);
}
conclusion = conclusion1;
pr = m.mk_hyper_resolve(premises.size(), premises.c_ptr(), conclusion, positions, substs);
}
}
void boogie_proof::set_proof(proof* p) {
std::cout << "set proof\n";
m_proof = p;
proof_utils::push_instantiations_up(m_proof);
mk_input_resolution(m_proof);
std::cout << "proof set\n";
}
void boogie_proof::set_model(model* m) {
m_model = m;
}
void boogie_proof::pp(std::ostream& out) {
if (m_proof) {
pp_proof(out);
}
if (m_model) {
model_pp(out, *m_model);
}
}
void boogie_proof::pp_proof(std::ostream& out) {
vector<step> steps;
ptr_vector<proof> rules;
rules.push_back(m_proof);
steps.push_back(step());
obj_map<proof, unsigned> index;
index.insert(m_proof, 0);
for (unsigned j = 0; j < rules.size(); ++j) {
proof* p = rules[j];
proof_ref_vector premises(m);
expr_ref conclusion(m);
svector<std::pair<unsigned, unsigned> > positions;
vector<expr_ref_vector> substs;
expr* tmp;
steps[j].m_fact = m.get_fact(p);
m.is_implies(steps[j].m_fact, tmp, steps[j].m_fact);
get_subst(p, steps[j].m_subst);
get_labels(p, steps[j].m_labels);
if (m.is_hyper_resolve(p, premises, conclusion, positions, substs)) {
for (unsigned i = 1; i < premises.size(); ++i) {
proof* premise = premises[i].get();
unsigned position = 0;
if (!index.find(premise, position)) {
position = rules.size();
rules.push_back(premise);
steps.push_back(step());
index.insert(premise, position);
}
steps[j].m_refs.push_back(position);
}
get_rule_name(premises[0].get(), steps[j].m_rule_name);
}
}
for (unsigned j = steps.size(); j > 0; ) {
--j;
step &s = steps[j];
// TBD
s.m_labels;
// set references, compensate for reverse ordering.
for (unsigned i = 0; i < s.m_refs.size(); ++i) {
s.m_refs[i] = rules.size()-1-s.m_refs[i];
}
}
steps.reverse();
pp_steps(out, steps);
}
/**
\brief extract the instantiation by searching for the first occurrence of a hyper-resolution
rule that produces an instance.
*/
void boogie_proof::get_subst(proof* p, subst& s) {
ptr_vector<proof> todo;
todo.push_back(p);
ast_mark visited;
std::cout << "get_subst\n" << mk_pp(p, m) << "\n";
while (!todo.empty()) {
proof* p = todo.back();
todo.pop_back();
if (visited.is_marked(p)) {
continue;
}
visited.mark(p, true);
proof_ref_vector premises(m);
expr_ref conclusion(m);
svector<std::pair<unsigned, unsigned> > positions;
vector<expr_ref_vector> substs;
if (m.is_hyper_resolve(p, premises, conclusion, positions, substs)) {
expr_ref_vector const& sub = substs[0];
if (!sub.empty()) {
quantifier* q = to_quantifier(m.get_fact(premises[0].get()));
unsigned sz = sub.size();
SASSERT(sz == q->get_num_decls());
for (unsigned i = 0; i < sz; ++i) {
s.push_back(std::make_pair(q->get_decl_name(sz-1-i), sub[i]));
}
return;
}
}
unsigned sz = m.get_num_parents(p);
for (unsigned i = 0; i < sz; ++i) {
todo.push_back(m.get_parent(p, i));
}
}
}
void boogie_proof::get_rule_name(proof* p, symbol& n) {
}
void boogie_proof::get_labels(proof* p, labels& lbls) {
}
void boogie_proof::pp_steps(std::ostream& out, vector<step>& steps) {
out << "(derivation\n";
for (unsigned i = 0; i < steps.size(); ++i) {
pp_step(out, i, steps[i]);
}
out << ")\n";
}
// step :: "(" "step" step-name fact rule-name subst labels premises ")"
void boogie_proof::pp_step(std::ostream& out, unsigned id, step& s) {
out << "(step\n";
out << " s!" << id << " ";
pp_fact(out, s.m_fact);
out << " " << s.m_rule_name << "\n";
pp_subst(out << " ", s.m_subst);
pp_labels(out << " ", s.m_labels);
pp_premises(out << " ", s.m_refs);
out << ")\n";
}
// fact :: "(" predicate theory-term* ")"
void boogie_proof::pp_fact(std::ostream& out, expr* fact) {
out << mk_pp(fact, m) << "\n";
}
// subst :: "(" "subst" assignment* ")"
void boogie_proof::pp_subst(std::ostream& out, subst& s) {
out << "(subst";
for (unsigned i = 0; i < s.size(); ++i) {
pp_assignment(out, s[i].first, s[i].second);
}
out << ")\n";
}
// assignment :: "(" "=" variable theory-term ")"
void boogie_proof::pp_assignment(std::ostream& out, symbol const& v, expr* t) {
out << "\n (= " << v << " " << mk_pp(t, m) << ")";
}
// labels :: "(" "labels" label* ")"
void boogie_proof::pp_labels(std::ostream& out, labels& lbls) {
out << "(labels";
for (unsigned i = 0; i < lbls.size(); ++i) {
out << " " << lbls[i];
}
out << ")\n";
}
// premises "(" "ref" step-name* ")"
void boogie_proof::pp_premises(std::ostream& out, refs& refs) {
out << "(ref";
for (unsigned i = 0; i < refs.size(); ++i) {
out << " s!" << refs[i];
}
out << ")\n";
}
}

87
src/muz_qe/dl_boogie_proof.h Normal file
View file

@ -0,0 +1,87 @@
/**
output :: derivation model
derivation :: "(" "derivation" step* ")"
step :: "(" "step" step-name fact rule-name subst labels premises ")"
step-name :: identifier
rule-name :: identifier
fact :: "(" predicate theory-term* ")"
subst :: "(" "subst" assignment* ")"
assignment :: "(" "=" variable theory-term ")"
labels :: "(" "labels" label* ")"
premises :: "(" "ref" step-name* ")"
model :: "(" "model" smtlib2-model ")"
In each step the "fact" is derivable by hyper-resolution from the named
premises and the named rule, under the given substitution for the
universally quantified variables in the rule. The premises of each
step must have occurred previously in the step sequence. The last fact
is a nullary placeholder predicate representing satisfaction of the query
(its name is arbitrary).
The labels list consists of all the positively labeled sub-formulas whose
truth is used in the proof, and all the negatively labeled formulas whose
negation is used. A theory-term is a ground term using only interpreted
constants of the background theories.
The smtlib2-model gives an interpretation of the uninterpreted constants
in the background theory under which the derivation is valid. Currently
it is a quoted string in the old z3 model format, for compatibility with
Boogie, however, this should be changed to the new model format (using
define-fun) when Boogie supports this.
*/
#include "ast.h"
#include "model.h"
namespace datalog {
class boogie_proof {
typedef vector<std::pair<symbol,expr*> > subst;
typedef svector<symbol> labels;
typedef unsigned_vector refs;
struct step {
symbol m_rule_name;
expr* m_fact;
subst m_subst;
labels m_labels;
refs m_refs;
};
ast_manager& m;
proof_ref m_proof;
model_ref m_model;
void pp_proof(std::ostream& out);
void pp_steps(std::ostream& out, vector<step>& steps);
void pp_step(std::ostream& out, unsigned i, step& s);
void pp_fact(std::ostream& out, expr* fact);
void pp_subst(std::ostream& out, subst& s);
void pp_assignment(std::ostream& out, symbol const& v, expr* t);
void pp_labels(std::ostream& out, labels& lbls);
void pp_premises(std::ostream& out, refs& refs);
void get_subst(proof* p, subst& sub);
void get_rule_name(proof* p, symbol&);
void get_labels(proof* p, labels&);
public:
boogie_proof(ast_manager& m): m(m), m_proof(m), m_model(0) {}
void set_proof(proof* p);
void set_model(model* m);
void pp(std::ostream& out);
};
}

4
src/muz_qe/dl_cmds.cpp
View file

@ -328,9 +328,7 @@ private:
void print_certificate(cmd_context& ctx) {
if (m_dl_ctx->get_params().print_certificate()) {
datalog::context& dlctx = m_dl_ctx->dlctx();
if (!dlctx.display_certificate(ctx.regular_stream())) {
throw cmd_exception("certificates are not supported for the selected engine");
}
dlctx.display_certificate(ctx.regular_stream());
ctx.regular_stream() << "\n";
}
}

8
src/muz_qe/dl_compiler.cpp
View file

@ -42,7 +42,7 @@ namespace datalog {
return;
}
relation_signature sig;
m_context.get_rel_context().get_rmanager().from_predicate(pred, sig);
m_context.get_rel_context()->get_rmanager().from_predicate(pred, sig);
reg_idx reg = get_fresh_register(sig);
e->get_data().m_value=reg;
@ -606,7 +606,7 @@ namespace datalog {
}
SASSERT(is_app(e));
relation_sort arg_sort;
m_context.get_rel_context().get_rmanager().from_predicate(neg_pred, i, arg_sort);
m_context.get_rel_context()->get_rmanager().from_predicate(neg_pred, i, arg_sort);
reg_idx new_reg;
bool new_dealloc;
make_add_constant_column(head_pred, filtered_res, arg_sort, to_app(e), new_reg, new_dealloc, acc);
@ -1252,7 +1252,7 @@ namespace datalog {
func_decl_set::iterator fdit = preds.begin();
func_decl_set::iterator fdend = preds.end();
for(; fdit!=fdend; ++fdit) {
if(!m_context.get_rel_context().get_rmanager().is_saturated(*fdit)) {
if(!m_context.get_rel_context()->get_rmanager().is_saturated(*fdit)) {
return false;
}
}
@ -1337,7 +1337,7 @@ namespace datalog {
acc.set_observer(0);
TRACE("dl", execution_code.display(m_context.get_rel_context(), tout););
TRACE("dl", execution_code.display(*m_context.get_rel_context(), tout););
}

331
src/muz_qe/dl_context.cpp
View file

@ -45,6 +45,7 @@ Revision History:
#include"dl_mk_bit_blast.h"
#include"dl_mk_array_blast.h"
#include"dl_mk_karr_invariants.h"
#include"dl_mk_magic_symbolic.h"
#include"dl_mk_quantifier_abstraction.h"
#include"dl_mk_quantifier_instantiation.h"
#include"datatype_decl_plugin.h"
@ -238,11 +239,13 @@ namespace datalog {
m_rule_fmls(m),
m_background(m),
m_mc(0),
m_rel(0),
m_engine(0),
m_closed(false),
m_saturation_was_run(false),
m_last_status(OK),
m_last_answer(m),
m_engine(LAST_ENGINE),
m_engine_type(LAST_ENGINE),
m_cancel(false) {
}
@ -260,8 +263,7 @@ namespace datalog {
m_preds.reset();
m_preds_by_name.reset();
reset_dealloc_values(m_sorts);
m_pdr = 0;
m_bmc = 0;
m_engine = 0;
m_rel = 0;
}
@ -432,8 +434,7 @@ namespace datalog {
void context::set_predicate_representation(func_decl * pred, unsigned relation_name_cnt,
symbol const * relation_names) {
if (relation_name_cnt > 0) {
ensure_rel();
if (m_rel && relation_name_cnt > 0) {
m_rel->set_predicate_representation(pred, relation_name_cnt, relation_names);
}
}
@ -445,7 +446,7 @@ namespace datalog {
register_predicate(new_pred, true);
if (m_rel.get()) {
if (m_rel) {
m_rel->inherit_predicate_kind(new_pred, orig_pred);
}
return new_pred;
@ -542,64 +543,18 @@ namespace datalog {
}
unsigned context::get_num_levels(func_decl* pred) {
switch(get_engine()) {
case DATALOG_ENGINE:
throw default_exception("get_num_levels is not supported for datalog engine");
case PDR_ENGINE:
case QPDR_ENGINE:
ensure_pdr();
return m_pdr->get_num_levels(pred);
case BMC_ENGINE:
case QBMC_ENGINE:
throw default_exception("get_num_levels is not supported for bmc");
case TAB_ENGINE:
throw default_exception("get_num_levels is not supported for tab");
case CLP_ENGINE:
throw default_exception("get_num_levels is not supported for clp");
default:
throw default_exception("unknown engine");
}
ensure_engine();
return m_engine->get_num_levels(pred);
}
expr_ref context::get_cover_delta(int level, func_decl* pred) {
switch(get_engine()) {
case DATALOG_ENGINE:
throw default_exception("operation is not supported for datalog engine");
case PDR_ENGINE:
case QPDR_ENGINE:
ensure_pdr();
return m_pdr->get_cover_delta(level, pred);
case BMC_ENGINE:
case QBMC_ENGINE:
throw default_exception("operation is not supported for BMC engine");
case TAB_ENGINE:
throw default_exception("operation is not supported for TAB engine");
case CLP_ENGINE:
throw default_exception("operation is not supported for CLP engine");
default:
throw default_exception("unknown engine");
}
ensure_engine();
return m_engine->get_cover_delta(level, pred);
}
void context::add_cover(int level, func_decl* pred, expr* property) {
switch(get_engine()) {
case DATALOG_ENGINE:
throw default_exception("operation is not supported for datalog engine");
case PDR_ENGINE:
case QPDR_ENGINE:
ensure_pdr();
m_pdr->add_cover(level, pred, property);
break;
case BMC_ENGINE:
case QBMC_ENGINE:
throw default_exception("operation is not supported for BMC engine");
case TAB_ENGINE:
throw default_exception("operation is not supported for TAB engine");
case CLP_ENGINE:
throw default_exception("operation is not supported for CLP engine");
default:
throw default_exception("unknown engine");
}
ensure_engine();
m_engine->add_cover(level, pred, property);
}
void context::check_uninterpreted_free(rule_ref& r) {
@ -743,7 +698,7 @@ namespace datalog {
void context::add_fact(func_decl * pred, const relation_fact & fact) {
if (get_engine() == DATALOG_ENGINE) {
ensure_rel();
ensure_engine();
m_rel->add_fact(pred, fact);
}
else {
@ -769,7 +724,7 @@ namespace datalog {
void context::add_table_fact(func_decl * pred, const table_fact & fact) {
if (get_engine() == DATALOG_ENGINE) {
ensure_rel();
ensure_engine();
m_rel->add_fact(pred, fact);
}
else {
@ -907,6 +862,9 @@ namespace datalog {
m_transf.register_plugin(alloc(datalog::mk_bit_blast, *this, 35000));
m_transf.register_plugin(alloc(datalog::mk_array_blast, *this, 36000));
m_transf.register_plugin(alloc(datalog::mk_karr_invariants, *this, 36010));
if (get_params().magic()) {
m_transf.register_plugin(alloc(datalog::mk_magic_symbolic, *this, 36020));
}
transform_rules(m_transf);
}
@ -917,7 +875,7 @@ namespace datalog {
void context::updt_params(params_ref const& p) {
m_params_ref.copy(p);
if (m_pdr.get()) m_pdr->updt_params();
if (m_engine.get()) m_engine->updt_params();
}
expr_ref context::get_background_assertion() {
@ -940,45 +898,39 @@ namespace datalog {
m_cancel = true;
m_last_status = CANCELED;
m_transf.cancel();
if (m_pdr.get()) m_pdr->cancel();
if (m_bmc.get()) m_bmc->cancel();
if (m_tab.get()) m_tab->cancel();
if (m_rel.get()) m_rel->set_cancel(true);
if (m_engine) m_engine->cancel();
}
void context::cleanup() {
m_cancel = false;
m_last_status = OK;
if (m_pdr.get()) m_pdr->cleanup();
if (m_bmc.get()) m_bmc->cleanup();
if (m_tab.get()) m_tab->cleanup();
if (m_rel.get()) m_rel->set_cancel(false);
if (m_engine) m_engine->cleanup();
}
class context::engine_type_proc {
ast_manager& m;
arith_util a;
datatype_util dt;
DL_ENGINE m_engine;
DL_ENGINE m_engine_type;
public:
engine_type_proc(ast_manager& m): m(m), a(m), dt(m), m_engine(DATALOG_ENGINE) {}
engine_type_proc(ast_manager& m): m(m), a(m), dt(m), m_engine_type(DATALOG_ENGINE) {}
DL_ENGINE get_engine() const { return m_engine; }
DL_ENGINE get_engine() const { return m_engine_type; }
void operator()(expr* e) {
if (is_quantifier(e)) {
m_engine = QPDR_ENGINE;
m_engine_type = QPDR_ENGINE;
}
else if (m_engine != QPDR_ENGINE) {
else if (m_engine_type != QPDR_ENGINE) {
if (a.is_int_real(e)) {
m_engine = PDR_ENGINE;
m_engine_type = PDR_ENGINE;
}
else if (is_var(e) && m.is_bool(e)) {
m_engine = PDR_ENGINE;
m_engine_type = PDR_ENGINE;
}
else if (dt.is_datatype(m.get_sort(e))) {
m_engine = PDR_ENGINE;
m_engine_type = PDR_ENGINE;
}
}
}
@ -988,46 +940,46 @@ namespace datalog {
symbol e = m_params.engine();
if (e == symbol("datalog")) {
m_engine = DATALOG_ENGINE;
m_engine_type = DATALOG_ENGINE;
}
else if (e == symbol("pdr")) {
m_engine = PDR_ENGINE;
m_engine_type = PDR_ENGINE;
}
else if (e == symbol("qpdr")) {
m_engine = QPDR_ENGINE;
m_engine_type = QPDR_ENGINE;
}
else if (e == symbol("bmc")) {
m_engine = BMC_ENGINE;
m_engine_type = BMC_ENGINE;
}
else if (e == symbol("qbmc")) {
m_engine = QBMC_ENGINE;
m_engine_type = QBMC_ENGINE;
}
else if (e == symbol("tab")) {
m_engine = TAB_ENGINE;
m_engine_type = TAB_ENGINE;
}
else if (e == symbol("clp")) {
m_engine = CLP_ENGINE;
m_engine_type = CLP_ENGINE;
}
if (m_engine == LAST_ENGINE) {
if (m_engine_type == LAST_ENGINE) {
expr_fast_mark1 mark;
engine_type_proc proc(m);
m_engine = DATALOG_ENGINE;
for (unsigned i = 0; m_engine == DATALOG_ENGINE && i < m_rule_set.get_num_rules(); ++i) {
m_engine_type = DATALOG_ENGINE;
for (unsigned i = 0; m_engine_type == DATALOG_ENGINE && i < m_rule_set.get_num_rules(); ++i) {
rule * r = m_rule_set.get_rule(i);
quick_for_each_expr(proc, mark, r->get_head());
for (unsigned j = 0; j < r->get_tail_size(); ++j) {
quick_for_each_expr(proc, mark, r->get_tail(j));
}
m_engine = proc.get_engine();
m_engine_type = proc.get_engine();
}
for (unsigned i = m_rule_fmls_head; m_engine == DATALOG_ENGINE && i < m_rule_fmls.size(); ++i) {
for (unsigned i = m_rule_fmls_head; m_engine_type == DATALOG_ENGINE && i < m_rule_fmls.size(); ++i) {
expr* fml = m_rule_fmls[i].get();
while (is_quantifier(fml)) {
fml = to_quantifier(fml)->get_expr();
}
quick_for_each_expr(proc, mark, fml);
m_engine = proc.get_engine();
m_engine_type = proc.get_engine();
}
}
}
@ -1038,170 +990,78 @@ namespace datalog {
m_last_answer = 0;
switch (get_engine()) {
case DATALOG_ENGINE:
flush_add_rules();
return rel_query(query);
case PDR_ENGINE:
case QPDR_ENGINE:
flush_add_rules();
return pdr_query(query);
case BMC_ENGINE:
case QBMC_ENGINE:
flush_add_rules();
return bmc_query(query);
case TAB_ENGINE:
flush_add_rules();
return tab_query(query);
case CLP_ENGINE:
flush_add_rules();
return clp_query(query);
break;
default:
UNREACHABLE();
return rel_query(query);
}
ensure_engine();
return m_engine->query(query);
}
model_ref context::get_model() {
switch(get_engine()) {
case PDR_ENGINE:
case QPDR_ENGINE:
ensure_pdr();
return m_pdr->get_model();
default:
return model_ref(alloc(model, m));
}
ensure_engine();
return m_engine->get_model();
}
proof_ref context::get_proof() {
switch(get_engine()) {
case PDR_ENGINE:
case QPDR_ENGINE:
ensure_pdr();
return m_pdr->get_proof();
default:
return proof_ref(m.mk_asserted(m.mk_true()), m);
}
ensure_engine();
return m_engine->get_proof();
}
void context::ensure_pdr() {
if (!m_pdr.get()) {
m_pdr = alloc(pdr::dl_interface, *this);
void context::ensure_engine() {
if (!m_engine.get()) {
switch (get_engine()) {
case PDR_ENGINE:
case QPDR_ENGINE:
m_engine = alloc(pdr::dl_interface, *this);
break;
case DATALOG_ENGINE:
m_rel = alloc(rel_context, *this);
m_engine = m_rel;
break;
case BMC_ENGINE:
case QBMC_ENGINE:
m_engine = alloc(bmc, *this);
break;
case TAB_ENGINE:
m_engine = alloc(tab, *this);
break;
case CLP_ENGINE:
m_engine = alloc(clp, *this);
break;
}
}
}
lbool context::pdr_query(expr* query) {
ensure_pdr();
return m_pdr->query(query);
}
void context::ensure_bmc() {
if (!m_bmc.get()) {
m_bmc = alloc(bmc, *this);
lbool context::rel_query(unsigned num_rels, func_decl * const* rels) {
ensure_engine();
if (m_rel) {
return m_rel->query(num_rels, rels);
}
else {
return l_undef;
}
}
lbool context::bmc_query(expr* query) {
ensure_bmc();
return m_bmc->query(query);
}
void context::ensure_tab() {
if (!m_tab.get()) {
m_tab = alloc(tab, *this);
}
}
void context::ensure_clp() {
if (!m_clp.get()) {
m_clp = alloc(clp, *this);
}
}
lbool context::tab_query(expr* query) {
ensure_tab();
return m_tab->query(query);
}
lbool context::clp_query(expr* query) {
ensure_clp();
return m_clp->query(query);
}
void context::ensure_rel() {
if (!m_rel.get()) {
m_rel = alloc(rel_context, *this);
}
}
lbool context::rel_query(unsigned num_rels, func_decl * const* rels) {
ensure_rel();
return m_rel->query(num_rels, rels);
}
lbool context::rel_query(expr* query) {
ensure_rel();
return m_rel->query(query);
}
expr* context::get_answer_as_formula() {
if (m_last_answer) {
return m_last_answer.get();
}
switch(get_engine()) {
case PDR_ENGINE:
case QPDR_ENGINE:
ensure_pdr();
m_last_answer = m_pdr->get_answer();
return m_last_answer.get();
case BMC_ENGINE:
case QBMC_ENGINE:
ensure_bmc();
m_last_answer = m_bmc->get_answer();
return m_last_answer.get();
case DATALOG_ENGINE:
ensure_rel();
m_last_answer = m_rel->get_last_answer();
return m_last_answer.get();
case TAB_ENGINE:
ensure_tab();
m_last_answer = m_tab->get_answer();
return m_last_answer.get();
case CLP_ENGINE:
ensure_clp();
m_last_answer = m_clp->get_answer();
return m_last_answer.get();
default:
UNREACHABLE();
}
m_last_answer = m.mk_false();
ensure_engine();
m_last_answer = m_engine->get_answer();
return m_last_answer.get();
}
bool context::display_certificate(std::ostream& out) {
switch(get_engine()) {
case DATALOG_ENGINE:
return false;
case PDR_ENGINE:
case QPDR_ENGINE:
ensure_pdr();
m_pdr->display_certificate(out);
return true;
case BMC_ENGINE:
case QBMC_ENGINE:
ensure_bmc();
m_bmc->display_certificate(out);
return true;
case TAB_ENGINE:
ensure_tab();
m_tab->display_certificate(out);
return true;
case CLP_ENGINE:
ensure_clp();
m_clp->display_certificate(out);
return true;
default:
return false;
}
void context::display_certificate(std::ostream& out) {
ensure_engine();
m_engine->display_certificate(out);
}
void context::display_profile(std::ostream& out) const {
@ -1219,26 +1079,14 @@ namespace datalog {
}
void context::reset_statistics() {
if (m_pdr) {
m_pdr->reset_statistics();
}
if (m_bmc) {
m_bmc->reset_statistics();
}
if (m_tab) {
m_tab->reset_statistics();
if (m_engine) {
m_engine->reset_statistics();
}
}
void context::collect_statistics(statistics& st) const {
if (m_pdr) {
m_pdr->collect_statistics(st);
}
if (m_bmc) {
m_bmc->collect_statistics(st);
}
if (m_tab) {
m_tab->collect_statistics(st);
if (m_engine) {
m_engine->collect_statistics(st);
}
}
@ -1246,8 +1094,7 @@ namespace datalog {
execution_result context::get_status() { return m_last_status; }
bool context::result_contains_fact(relation_fact const& f) {
ensure_rel();
return m_rel->result_contains_fact(f);
return m_rel && m_rel->result_contains_fact(f);
}
// NB: algebraic data-types declarations will not be printed.

35
src/muz_qe/dl_context.h
View file

@ -121,17 +121,14 @@ namespace datalog {
model_converter_ref m_mc;
proof_converter_ref m_pc;
scoped_ptr<pdr::dl_interface> m_pdr;
scoped_ptr<bmc> m_bmc;
scoped_ptr<rel_context> m_rel;
scoped_ptr<tab> m_tab;
scoped_ptr<clp> m_clp;
rel_context* m_rel;
scoped_ptr<engine_base> m_engine;
bool m_closed;
bool m_saturation_was_run;
execution_result m_last_status;
expr_ref m_last_answer;
DL_ENGINE m_engine;
DL_ENGINE m_engine_type;
volatile bool m_cancel;
@ -161,7 +158,7 @@ namespace datalog {
rule_manager & get_rule_manager() { return m_rule_manager; }
smt_params & get_fparams() const { return m_fparams; }
fixedpoint_params const& get_params() const { return m_params; }
DL_ENGINE get_engine() { configure_engine(); return m_engine; }
DL_ENGINE get_engine() { configure_engine(); return m_engine_type; }
th_rewriter& get_rewriter() { return m_rewriter; }
var_subst & get_var_subst() { return m_var_subst; }
dl_decl_util & get_decl_util() { return m_decl_util; }
@ -454,14 +451,14 @@ namespace datalog {
/**
\brief Display a certificate for reachability and/or unreachability.
*/
bool display_certificate(std::ostream& out);
void display_certificate(std::ostream& out);
/**
\brief query result if it contains fact.
*/
bool result_contains_fact(relation_fact const& f);
rel_context& get_rel_context() { ensure_rel(); return *m_rel; }
rel_context* get_rel_context() { ensure_engine(); return m_rel; }
private:
@ -473,25 +470,7 @@ namespace datalog {
void flush_add_rules();
void ensure_pdr();
void ensure_bmc();
void ensure_tab();
void ensure_clp();
void ensure_rel();
lbool rel_query(expr* query);
lbool pdr_query(expr* query);
lbool bmc_query(expr* query);
lbool tab_query(expr* query);
lbool clp_query(expr* query);
void ensure_engine();
void check_quantifier_free(rule_ref& r);
void check_uninterpreted_free(rule_ref& r);

2
src/muz_qe/dl_instruction.cpp
View file

@ -59,7 +59,7 @@ namespace datalog {
}
rel_context& execution_context::get_rel_context() {
return m_context.get_rel_context();
return *m_context.get_rel_context();
}
struct compare_size_proc {

2
src/muz_qe/dl_mk_backwards.cpp
View file

@ -48,7 +48,7 @@ namespace datalog {
neg.reset();
rule & r = *source.get_rule(i);
unsigned utsz = r.get_uninterpreted_tail_size();
unsigned tsz = r.get_tail_size();
unsigned tsz = r.get_tail_size();
if (!source.is_output_predicate(r.get_decl())) {
tail.push_back(r.get_head());
neg.push_back(false);

6
src/muz_qe/dl_mk_explanations.cpp
View file

@ -604,7 +604,7 @@ namespace datalog {
m_e_sort = m_decl_util.mk_rule_sort();
m_pinned.push_back(m_e_sort);
relation_manager & rmgr = ctx.get_rel_context().get_rmanager();
relation_manager & rmgr = ctx.get_rel_context()->get_rmanager();
symbol er_symbol = explanation_relation_plugin::get_name(m_relation_level);
m_er_plugin = static_cast<explanation_relation_plugin *>(rmgr.get_relation_plugin(er_symbol));
if (!m_er_plugin) {
@ -637,7 +637,7 @@ namespace datalog {
void mk_explanations::assign_rel_level_kind(func_decl * e_decl, func_decl * orig) {
SASSERT(m_relation_level);
relation_manager & rmgr = m_context.get_rel_context().get_rmanager();
relation_manager & rmgr = m_context.get_rel_context()->get_rmanager();
unsigned sz = e_decl->get_arity();
relation_signature sig;
rmgr.from_predicate(e_decl, sig);
@ -871,7 +871,7 @@ namespace datalog {
return 0;
}
rule_set * res = alloc(rule_set, m_context);
transform_facts(m_context.get_rel_context().get_rmanager(), source, *res);
transform_facts(m_context.get_rel_context()->get_rmanager(), source, *res);
transform_rules(source, *res);
return res;
}

10
src/muz_qe/dl_mk_karr_invariants.cpp
View file

@ -49,7 +49,8 @@ namespace datalog {
rm(ctx.get_rule_manager()),
m_inner_ctx(m, ctx.get_fparams()),
a(m),
m_pinned(m) {
m_pinned(m),
m_cancel(false) {
params_ref params;
params.set_sym("default_relation", symbol("karr_relation"));
params.set_sym("engine", symbol("datalog"));
@ -189,6 +190,7 @@ namespace datalog {
};
void mk_karr_invariants::cancel() {
m_cancel = true;
m_inner_ctx.cancel();
}
@ -211,6 +213,10 @@ namespace datalog {
get_invariants(*src_loop);
if (m_cancel) {
return 0;
}
// figure out whether to update same rules as used for saturation.
scoped_ptr<rule_set> rev_source = bwd(*src_loop);
get_invariants(*rev_source);
@ -225,7 +231,7 @@ namespace datalog {
void mk_karr_invariants::get_invariants(rule_set const& src) {
m_inner_ctx.reset();
rel_context& rctx = m_inner_ctx.get_rel_context();
rel_context& rctx = *m_inner_ctx.get_rel_context();
ptr_vector<func_decl> heads;
func_decl_set const& predicates = m_ctx.get_predicates();
for (func_decl_set::iterator fit = predicates.begin(); fit != predicates.end(); ++fit) {

1
src/muz_qe/dl_mk_karr_invariants.h
View file

@ -57,6 +57,7 @@ namespace datalog {
arith_util a;
obj_map<func_decl, expr*> m_fun2inv;
ast_ref_vector m_pinned;
volatile bool m_cancel;
void get_invariants(rule_set const& src);

2
src/muz_qe/dl_mk_magic_sets.cpp
View file

@ -362,7 +362,7 @@ namespace datalog {
rule * r = *it;
transform_rule(task.m_adornment, r, *result);
}
if (!m_context.get_rel_context().get_relation(task.m_pred).empty()) {
if (!m_context.get_rel_context()->get_relation(task.m_pred).empty()) {
//we need a rule to copy facts that are already in a relation into the adorned
//relation (since out intentional predicates can have facts, not only rules)
create_transfer_rule(task, *result);

133
src/muz_qe/dl_mk_magic_symbolic.cpp Normal file
View file

@ -0,0 +1,133 @@
/*++
Copyright (c) 2013 Microsoft Corporation
Module Name:
dl_mk_magic_symbolic.cpp
Abstract:
Create Horn clauses for magic symbolic flow.
Q(x) :- A(y), B(z), phi1(x,y,z).
Q(x) :- C(y), phi2(x,y).
A(x) :- C(y), phi3(x,y).
A(x) :- A(y), phi3(x,y).
B(x) :- C(y), A(z), phi4(x,y,z).
C(x) :- phi5(x).
Transformed clauses:
Q_ans(x) :- Q_query(x), A_ans(y), B_ans(z), phi1(x,y,z).
Q_ans(x) :- Q_query(x), C_ans(y), phi2(x,y).
Q_query(x) :- true.
A_ans(x) :- A_query(x), C_ans(y), phi2(x,y)
A_ans(x) :- A_query(x), A_ans(y), phi3(x,y).
A_query(y) :- Q_query(x), phi1(x,y,z).
A_query(y) :- A_query(x), phi3(x,y).
A_query(z) :- B_query(x), C_ans(y), phi4(x,y,z).
B_ans(x) :- B_query(x), C_ans(y), A_ans(z), phi4(x,y,z).
B_query(z) :- Q_query(x), A_ans(y), phi1(x,y,z).
C_ans(x) :- C_query(x), phi5(x).
C_query(y) :- Q_query(x), phi2(x,y).
C_query(y) :- Q_query(x), phi3(x,y).
C_query(y) :- B_query(x), phi4(x,y,z).
General scheme:
A(x) :- P1(x_1), ..., Pn(x_n), phi(x,x1,..,x_n).
P(x) :- Prefix(x,y,z), A(z) ...
A_ans(x) :- A_query(x), P_i_ans(x_i), phi(x,..).
A_query(z) :- P_query(x), Prefix_ans(x,y,z).
Author:
Nikolaj Bjorner (nbjorner) 2013-06-19
Revision History:
--*/
#include"dl_mk_magic_symbolic.h"
#include"dl_context.h"
namespace datalog {
mk_magic_symbolic::mk_magic_symbolic(context & ctx, unsigned priority):
plugin(priority),
m(ctx.get_manager()),
m_ctx(ctx) {
}
mk_magic_symbolic::~mk_magic_symbolic() { }
rule_set * mk_magic_symbolic::operator()(rule_set const & source) {
if (!m_ctx.get_params().magic()) {
return 0;
}
context& ctx = source.get_context();
rule_manager& rm = source.get_rule_manager();
rule_set * result = alloc(rule_set, ctx);
unsigned sz = source.get_num_rules();
rule_ref new_rule(rm);
app_ref_vector tail(m);
app_ref head(m);
svector<bool> neg;
for (unsigned i = 0; i < sz; ++i) {
rule & r = *source.get_rule(i);
unsigned utsz = r.get_uninterpreted_tail_size();
unsigned tsz = r.get_tail_size();
tail.reset();
neg.reset();
for (unsigned j = utsz; j < tsz; ++j) {
tail.push_back(r.get_tail(j));
neg.push_back(false);
}
tail.push_back(mk_query(r.get_head()));
neg.push_back(false);
for (unsigned j = 0; j < utsz; ++j) {
tail.push_back(mk_ans(r.get_tail(j)));
neg.push_back(false);
}
new_rule = rm.mk(mk_ans(r.get_head()), tail.size(), tail.c_ptr(), neg.c_ptr(), r.name(), true);
if (source.is_output_predicate(r.get_decl())) {
result->set_output_predicate(new_rule->get_decl());
}
result->add_rule(new_rule);
for (unsigned j = 0; j < utsz; ++j) {
new_rule = rm.mk(mk_query(r.get_tail(j)), tail.size()-utsz+j, tail.c_ptr(), neg.c_ptr(), r.name(), true);
result->add_rule(new_rule);
}
}
TRACE("dl", result->display(tout););
return result;
}
app_ref mk_magic_symbolic::mk_query(app* q) {
string_buffer<64> name;
func_decl* f = q->get_decl();
name << f->get_name() << "!query";
func_decl_ref g(m);
g = m.mk_func_decl(symbol(name.c_str()), f->get_arity(), f->get_domain(), f->get_range());
m_ctx.register_predicate(g, false);
return app_ref(m.mk_app(g, q->get_num_args(), q->get_args()), m);
}
app_ref mk_magic_symbolic::mk_ans(app* q) {
string_buffer<64> name;
func_decl* f = q->get_decl();
func_decl_ref g(m);
name << f->get_name() << "!ans";
g = m.mk_func_decl(symbol(name.c_str()), f->get_arity(), f->get_domain(), f->get_range());
m_ctx.register_predicate(g, false);
return app_ref(m.mk_app(g, q->get_num_args(), q->get_args()), m);
}
};

40
src/muz_qe/dl_mk_magic_symbolic.h Normal file
View file

@ -0,0 +1,40 @@
/*++
Copyright (c) 2013 Microsoft Corporation
Module Name:
dl_mk_magic_symbolic.h
Abstract:
Create Horn clauses for magic symbolic transformation.
Author:
Nikolaj Bjorner (nbjorner) 2013-06-19
Revision History:
--*/
#ifndef _DL_MK_MAGIC_SYMBOLIC_H_
#define _DL_MK_MAGIC_SYMBOLIC_H_
#include"dl_rule_transformer.h"
namespace datalog {
class mk_magic_symbolic : public rule_transformer::plugin {
ast_manager& m;
context& m_ctx;
app_ref mk_ans(app* q);
app_ref mk_query(app* q);
public:
mk_magic_symbolic(context & ctx, unsigned priority = 33037);
~mk_magic_symbolic();
rule_set * operator()(rule_set const & source);
};
};
#endif /* _DL_MK_MAGIC_SYMBOLIC_H_ */

2
src/muz_qe/dl_mk_partial_equiv.cpp
View file

@ -97,7 +97,7 @@ namespace datalog {
return 0;
}
relation_manager & rm = m_context.get_rel_context().get_rmanager();
relation_manager & rm = m_context.get_rel_context()->get_rmanager();
rule_set::decl2rules::iterator it = source.begin_grouped_rules();
rule_set::decl2rules::iterator end = source.end_grouped_rules();

5
src/muz_qe/dl_mk_rule_inliner.cpp
View file

@ -206,7 +206,10 @@ namespace datalog {
void mk_rule_inliner::count_pred_occurrences(rule_set const & orig)
{
m_context.get_rel_context().get_rmanager().collect_non_empty_predicates(m_preds_with_facts);
rel_context* rel = m_context.get_rel_context();
if (rel) {
rel->get_rmanager().collect_non_empty_predicates(m_preds_with_facts);
}
rule_set::iterator rend = orig.end();
for (rule_set::iterator rit = orig.begin(); rit!=rend; ++rit) {

2
src/muz_qe/dl_mk_similarity_compressor.cpp
View file

@ -368,7 +368,7 @@ namespace datalog {
collect_orphan_consts(*it, const_infos, val_fact);
m_context.add_fact(aux_pred, val_fact);
}
m_context.get_rel_context().get_rmanager().mark_saturated(aux_pred);
m_context.get_rel_context()->get_rmanager().mark_saturated(aux_pred);
app * new_head = r->get_head();
ptr_vector<app> new_tail;

8
src/muz_qe/dl_mk_simple_joins.cpp
View file

@ -570,11 +570,15 @@ namespace datalog {
cost estimate_size(app * t) const {
func_decl * pred = t->get_decl();
unsigned n=pred->get_arity();
relation_manager& rm = m_context.get_rel_context().get_rmanager();
rel_context* rel = m_context.get_rel_context();
if (!rel) {
return cost(1);
}
relation_manager& rm = rel->get_rmanager();
if( (m_context.saturation_was_run() && rm.try_get_relation(pred))
|| rm.is_saturated(pred)) {
SASSERT(rm.try_get_relation(pred)); //if it is saturated, it should exist
unsigned rel_size_int = m_context.get_rel_context().get_relation(pred).get_size_estimate_rows();
unsigned rel_size_int = rel->get_relation(pred).get_size_estimate_rows();
if(rel_size_int!=0) {
cost rel_size = static_cast<cost>(rel_size_int);
cost curr_size = rel_size;

6
src/muz_qe/dl_mk_subsumption_checker.cpp
View file

@ -249,7 +249,11 @@ namespace datalog {
}
void mk_subsumption_checker::scan_for_relations_total_due_to_facts(rule_set const& source) {
relation_manager& rm = m_context.get_rel_context().get_rmanager();
rel_context* rel = m_context.get_rel_context();
if (!rel) {
return;
}
relation_manager& rm = rel->get_rmanager();
decl_set const& candidate_preds = m_context.get_predicates();

6
src/muz_qe/dl_mk_unbound_compressor.cpp
View file

@ -334,8 +334,10 @@ namespace datalog {
// TODO mc
m_modified = false;
m_context.get_rel_context().get_rmanager().collect_non_empty_predicates(m_non_empty_rels);
rel_context* rel = m_context.get_rel_context();
if (rel) {
rel->get_rmanager().collect_non_empty_predicates(m_non_empty_rels);
}
unsigned init_rule_cnt = source.get_num_rules();
SASSERT(m_rules.empty());
for (unsigned i=0; i<init_rule_cnt; i++) {

62
src/muz_qe/dl_relation_manager.cpp
View file

@ -614,6 +614,60 @@ namespace datalog {
return t.get_plugin().mk_project_fn(t, col_cnt, removed_cols);
}
class relation_manager::default_relation_filter_interpreted_and_project_fn : public relation_transformer_fn {
scoped_ptr<relation_mutator_fn> m_filter;
scoped_ptr<relation_transformer_fn> m_project;
unsigned_vector m_removed_cols;
public:
/**
This constructor should be used only if we know that the projection operation
exists for the result of the join.
*/
default_relation_filter_interpreted_and_project_fn(
relation_mutator_fn* filter,
unsigned removed_col_cnt,
const unsigned * removed_cols)
: m_filter(filter),
m_project(0),
m_removed_cols(removed_col_cnt, removed_cols) {}
virtual relation_base * operator()(const relation_base & t) {
scoped_rel<relation_base> t1 = t.clone();
(*m_filter)(*t1);
if( !m_project) {
relation_manager & rmgr = t1->get_plugin().get_manager();
m_project = rmgr.mk_project_fn(*t1, m_removed_cols.size(), m_removed_cols.c_ptr());
if (!m_project) {
throw default_exception("projection does not exist");
}
}
return (*m_project)(*t1);
}
};
relation_transformer_fn * relation_manager::mk_filter_interpreted_and_project_fn(
const relation_base & t, app * condition,
unsigned removed_col_cnt, const unsigned * removed_cols) {
relation_transformer_fn* res =
t.get_plugin().mk_filter_interpreted_and_project_fn(
t,
condition,
removed_col_cnt,
removed_cols);
if (!res) {
relation_mutator_fn* filter_fn = mk_filter_interpreted_fn(t, condition);
if (filter_fn) {
res = alloc(default_relation_filter_interpreted_and_project_fn,
filter_fn,
removed_col_cnt,
removed_cols);
}
}
return res;
}
class relation_manager::default_relation_join_project_fn : public relation_join_fn {
scoped_ptr<relation_join_fn> m_join;
@ -720,14 +774,6 @@ namespace datalog {
return t.get_plugin().mk_filter_interpreted_fn(t, condition);
}
relation_transformer_fn * relation_manager::mk_filter_interpreted_and_project_fn(const relation_base & t,
app * condition,
unsigned removed_col_cnt,
const unsigned * removed_cols) {
return t.get_plugin().mk_filter_interpreted_and_project_fn(t, condition, removed_col_cnt, removed_cols);
}
class relation_manager::default_relation_select_equal_and_project_fn : public relation_transformer_fn {
scoped_ptr<relation_mutator_fn> m_filter;
scoped_ptr<relation_transformer_fn> m_project;

1
src/muz_qe/dl_relation_manager.h
View file

@ -42,6 +42,7 @@ namespace datalog {
class default_relation_join_project_fn;
class default_relation_select_equal_and_project_fn;
class default_relation_intersection_filter_fn;
class default_relation_filter_interpreted_and_project_fn;
class auxiliary_table_transformer_fn;
class auxiliary_table_filter_fn;

38
src/muz_qe/dl_util.h
View file

@ -28,6 +28,8 @@ Revision History:
#include"substitution.h"
#include"fixedpoint_params.hpp"
#include"ast_counter.h"
#include"statistics.h"
#include"lbool.h"
namespace datalog {
@ -58,6 +60,42 @@ namespace datalog {
LAST_ENGINE
};
class engine_base {
ast_manager& m;
std::string m_name;
public:
engine_base(ast_manager& m, char const* name): m(m), m_name(name) {}
virtual ~engine_base() {}
virtual expr_ref get_answer() = 0;
virtual lbool query(expr* q) = 0;
virtual void reset_statistics() {}
virtual void display_profile(std::ostream& out) const {}
virtual void collect_statistics(statistics& st) const {}
virtual unsigned get_num_levels(func_decl* pred) {
throw default_exception(std::string("get_num_levels is not supported for ") + m_name);
}
virtual expr_ref get_cover_delta(int level, func_decl* pred) {
throw default_exception(std::string("operation is not supported for ") + m_name);
}
virtual void add_cover(int level, func_decl* pred, expr* property) {
throw default_exception(std::string("operation is not supported for ") + m_name);
}
virtual void display_certificate(std::ostream& out) const {
throw default_exception(std::string("certificates are not supported for ") + m_name);
}
virtual model_ref get_model() {
return model_ref(alloc(model, m));
}
virtual proof_ref get_proof() {
return proof_ref(m.mk_asserted(m.mk_true()), m);
}
virtual void updt_params() {}
virtual void cancel() {}
virtual void cleanup() {}
};
struct std_string_hash_proc {
unsigned operator()(const std::string & s) const
{ return string_hash(s.c_str(), static_cast<unsigned>(s.length()), 17); }

2
src/muz_qe/fixedpoint_params.pyg
View file

@ -10,6 +10,7 @@ def_module_params('fixedpoint',
('bit_blast', BOOL, False, '(PDR) bit-blast bit-vectors'),
('explanations_on_relation_level', BOOL, False, '(DATALOG) if true, explanations are generated as history of each relation, rather than per fact (generate_explanations must be set to true for this option to have any effect)'),
('magic_sets_for_queries', BOOL, False, "(DATALOG) magic set transformation will be used for queries"),
('magic', BOOL, False, "perform symbolic magic set transformation"),
('unbound_compressor', BOOL, True, "auxiliary relations will be introduced to avoid unbound variables in rule heads"),
('similarity_compressor', BOOL, True, "(DATALOG) rules that differ only in values of constants will be merged into a single rule"),
('similarity_compressor_threshold', UINT, 11, "(DATALOG) if similarity_compressor is on, this value determines how many similar rules there must be in order for them to be merged"),
@ -60,6 +61,7 @@ def_module_params('fixedpoint',
"by putting in half of the table columns, if it would have been empty otherwise"),
('print_answer', BOOL, False, 'print answer instance(s) to query'),
('print_certificate', BOOL, False, 'print certificate for reachability or non-reachability'),
('print_boogie_certificate', BOOL, False, 'print certificate for reachability or non-reachability using a format understood by Boogie'),
('print_statistics', BOOL, False, 'print statistics'),
('use_utvpi', BOOL, True, 'PDR: Enable UTVPI strategy'),
('tab_selection', SYMBOL, 'weight', 'selection method for tabular strategy: weight (default), first, var-use'),

29
src/muz_qe/pdr_context.cpp
View file

@ -44,6 +44,7 @@ Notes:
#include "proof_checker.h"
#include "smt_value_sort.h"
#include "proof_utils.h"
#include "dl_boogie_proof.h"
namespace pdr {
@ -1063,7 +1064,7 @@ namespace pdr {
ast_manager& m = pt.get_manager();
datalog::context& dctx = ctx.get_context();
datalog::rule_manager& rm = dctx.get_rule_manager();
datalog::rule_unifier unifier(dctx);
datalog::rule_unifier unif(dctx);
datalog::dl_decl_util util(m);
datalog::rule_ref r0(rm), r1(rm);
obj_map<expr, proof*> cache;
@ -1072,7 +1073,7 @@ namespace pdr {
proof_ref_vector trail(m);
datalog::rule_ref_vector rules_trail(rm);
proof* pr = 0;
unifier.set_normalize(false);
unif.set_normalize(true);
todo.push_back(m_root);
update_models();
while (!todo.empty()) {
@ -1134,14 +1135,14 @@ namespace pdr {
substs.push_back(binding); // TODO base substitution.
for (unsigned i = 1; i < rls.size(); ++i) {
datalog::rule& src = *rls[i];
bool unified = unifier.unify_rules(*reduced_rule, 0, src);
bool unified = unif.unify_rules(*reduced_rule, 0, src);
if (!unified) {
IF_VERBOSE(0,
verbose_stream() << "Could not unify rules: ";
reduced_rule->display(dctx, verbose_stream());
src.display(dctx, verbose_stream()););
}
expr_ref_vector sub1 = unifier.get_rule_subst(*reduced_rule, true);
expr_ref_vector sub1 = unif.get_rule_subst(*reduced_rule, true);
TRACE("pdr",
for (unsigned k = 0; k < sub1.size(); ++k) {
tout << mk_pp(sub1[k].get(), m) << " ";
@ -1160,8 +1161,8 @@ namespace pdr {
}
positions.push_back(std::make_pair(i,0));
substs.push_back(unifier.get_rule_subst(src, false));
VERIFY(unifier.apply(*reduced_rule.get(), 0, src, r3));
substs.push_back(unif.get_rule_subst(src, false));
VERIFY(unif.apply(*reduced_rule.get(), 0, src, r3));
reduced_rule = r3;
}
@ -1620,6 +1621,12 @@ namespace pdr {
IF_VERBOSE(1, verbose_stream() << "\n"; m_search.display(verbose_stream()););
m_last_result = l_true;
validate();
IF_VERBOSE(1,
if (m_params.print_boogie_certificate()) {
display_certificate(verbose_stream());
});
return l_true;
}
catch (inductive_exception) {
@ -2129,7 +2136,15 @@ namespace pdr {
break;
}
case l_true: {
strm << mk_pp(mk_sat_answer(), m);
if (m_params.print_boogie_certificate()) {
datalog::boogie_proof bp(m);
bp.set_proof(get_proof());
bp.set_model(0);
bp.pp(strm);
}
else {
strm << mk_pp(mk_sat_answer(), m);
}
break;
}
case l_undef: {

1
src/muz_qe/pdr_dl_interface.cpp
View file

@ -37,6 +37,7 @@ Revision History:
using namespace pdr;
dl_interface::dl_interface(datalog::context& ctx) :
engine_base(ctx.get_manager(), "pdr"),
m_ctx(ctx),
m_pdr_rules(ctx),
m_old_rules(ctx),

29
src/muz_qe/pdr_dl_interface.h
View file

@ -23,6 +23,7 @@ Revision History:
#include "lbool.h"
#include "dl_rule.h"
#include "dl_rule_set.h"
#include "dl_util.h"
#include "statistics.h"
namespace datalog {
@ -33,7 +34,7 @@ namespace pdr {
class context;
class dl_interface {
class dl_interface : public datalog::engine_base {
datalog::context& m_ctx;
datalog::rule_set m_pdr_rules;
datalog::rule_set m_old_rules;
@ -47,31 +48,31 @@ namespace pdr {
dl_interface(datalog::context& ctx);
~dl_interface();
lbool query(expr* query);
virtual lbool query(expr* query);
void cancel();
virtual void cancel();
void cleanup();
virtual void cleanup();
void display_certificate(std::ostream& out) const;
virtual void display_certificate(std::ostream& out) const;
void collect_statistics(statistics& st) const;
virtual void collect_statistics(statistics& st) const;
void reset_statistics();
virtual void reset_statistics();
expr_ref get_answer();
virtual expr_ref get_answer();
unsigned get_num_levels(func_decl* pred);
virtual unsigned get_num_levels(func_decl* pred);
expr_ref get_cover_delta(int level, func_decl* pred);
virtual expr_ref get_cover_delta(int level, func_decl* pred);
void add_cover(int level, func_decl* pred, expr* property);
virtual void add_cover(int level, func_decl* pred, expr* property);
void updt_params();
virtual void updt_params();
model_ref get_model();
virtual model_ref get_model();
proof_ref get_proof();
virtual proof_ref get_proof();
};
}

129
src/muz_qe/pdr_generalizers.cpp
View file

@ -156,40 +156,19 @@ namespace pdr {
m_sigma.push_back(m.mk_fresh_const("sigma", a.mk_real()));
m_sigma.push_back(m.mk_fresh_const("sigma", a.mk_real()));
}
void core_convex_hull_generalizer::operator()(model_node& n, expr_ref_vector& core, bool& uses_level) {
method2(n, core, uses_level);
}
// use the entire region as starting point for generalization.
void core_convex_hull_generalizer::method1(model_node& n, expr_ref_vector& core, bool& uses_level) {
manager& pm = n.pt().get_pdr_manager();
expr_ref_vector conv1(m), conv2(m), core1(m), core2(m), eqs(m);
if (core.empty()) {
return;
}
if (!m_left.contains(n.pt().head())) {
expr_ref left(m), right(m);
m_left.insert(n.pt().head(), 0);
unsigned sz = n.pt().sig_size();
for (unsigned i = 0; i < sz; ++i) {
func_decl* fn0 = n.pt().sig(i);
sort* srt = fn0->get_range();
if (a.is_int_real(srt)) {
func_decl* fn1 = pm.o2n(fn0, 0);
left = m.mk_fresh_const(fn1->get_name().str().c_str(), srt);
right = m.mk_fresh_const(fn1->get_name().str().c_str(), srt);
m_left.insert(fn1, left);
m_right.insert(fn1, right);
m_trail.push_back(left);
m_trail.push_back(right);
}
}
}
unsigned sz = n.pt().sig_size();
for (unsigned i = 0; i < sz; ++i) {
expr* left, *right;
func_decl* fn0 = n.pt().sig(i);
func_decl* fn1 = pm.o2n(fn0, 0);
if (m_left.find(fn1, left) && m_right.find(fn1, right)) {
eqs.push_back(m.mk_eq(m.mk_const(fn1), a.mk_add(left, right)));
}
}
add_variables(n, eqs);
if (!mk_convex(core, 0, conv1)) {
IF_VERBOSE(0, verbose_stream() << "Non-convex: " << mk_pp(pm.mk_and(core), m) << "\n";);
return;
@ -230,6 +209,100 @@ namespace pdr {
}
}
// take as starting point two points from different regions.
void core_convex_hull_generalizer::method2(model_node& n, expr_ref_vector& core, bool& uses_level) {
expr_ref_vector conv1(m), conv2(m), core1(m), core2(m);
if (core.empty()) {
return;
}
manager& pm = n.pt().get_pdr_manager();
smt::kernel ctx(m, m_ctx.get_fparams(), m_ctx.get_params().p);
expr_ref goal(pm.mk_and(core));
ctx.assert_expr(goal);
lbool r = ctx.check();
if (r != l_true) {
IF_VERBOSE(0, verbose_stream() << "unexpected result from satisfiability check\n";);
return;
}
add_variables(n, conv1);
model_ref mdl;
ctx.get_model(mdl);
unsigned sz = n.pt().sig_size();
for (unsigned i = 0; i < sz; ++i) {
expr_ref_vector constr(m);
expr* left, *right;
func_decl* fn0 = n.pt().sig(i);
func_decl* fn1 = pm.o2n(fn0, 0);
if (m_left.find(fn1, left) && m_right.find(fn1, right)) {
expr_ref val(m);
mdl->eval(fn1, val);
if (val) {
conv1.push_back(m.mk_eq(left, val));
constr.push_back(m.mk_eq(right, val));
}
}
expr_ref new_model = pm.mk_and(constr);
m_trail.push_back(new_model);
m_trail.push_back(goal);
m_models.insert(goal, new_model);
}
conv1.push_back(a.mk_gt(m_sigma[0].get(), a.mk_numeral(rational(0), a.mk_real())));
conv1.push_back(a.mk_gt(m_sigma[1].get(), a.mk_numeral(rational(0), a.mk_real())));
conv1.push_back(m.mk_eq(a.mk_numeral(rational(1), a.mk_real()), a.mk_add(m_sigma[0].get(), m_sigma[1].get())));
obj_map<expr, expr*>::iterator it = m_models.begin(), end = m_models.end();
for (; it != end; ++it) {
if (it->m_key == goal) {
continue;
}
conv1.push_back(it->m_value);
expr_ref state = pm.mk_and(conv1);
TRACE("pdr", tout << "Try:\n" << mk_pp(state, m) << "\n";);
model_node nd(0, state, n.pt(), n.level());
if (l_false == n.pt().is_reachable(nd, &conv2, uses_level)) {
IF_VERBOSE(0,
verbose_stream() << mk_pp(state, m) << "\n";
verbose_stream() << "Generalized to:\n" << mk_pp(pm.mk_and(conv2), m) << "\n";);
core.reset();
core.append(conv2);
return;
}
conv1.pop_back();
}
}
void core_convex_hull_generalizer::add_variables(model_node& n, expr_ref_vector& eqs) {
manager& pm = n.pt().get_pdr_manager();
if (!m_left.contains(n.pt().head())) {
expr_ref left(m), right(m);
m_left.insert(n.pt().head(), 0);
unsigned sz = n.pt().sig_size();
for (unsigned i = 0; i < sz; ++i) {
func_decl* fn0 = n.pt().sig(i);
sort* srt = fn0->get_range();
if (a.is_int_real(srt)) {
func_decl* fn1 = pm.o2n(fn0, 0);
left = m.mk_fresh_const(fn1->get_name().str().c_str(), srt);
right = m.mk_fresh_const(fn1->get_name().str().c_str(), srt);
m_left.insert(fn1, left);
m_right.insert(fn1, right);
m_trail.push_back(left);
m_trail.push_back(right);
}
}
}
unsigned sz = n.pt().sig_size();
for (unsigned i = 0; i < sz; ++i) {
expr* left, *right;
func_decl* fn0 = n.pt().sig(i);
func_decl* fn1 = pm.o2n(fn0, 0);
if (m_left.find(fn1, left) && m_right.find(fn1, right)) {
eqs.push_back(m.mk_eq(m.mk_const(fn1), a.mk_add(left, right)));
}
}
}
bool core_convex_hull_generalizer::mk_convex(expr_ref_vector const& core, unsigned index, expr_ref_vector& conv) {
conv.reset();
for (unsigned i = 0; i < core.size(); ++i) {

4
src/muz_qe/pdr_generalizers.h
View file

@ -80,10 +80,14 @@ namespace pdr {
expr_ref_vector m_trail;
obj_map<func_decl, expr*> m_left;
obj_map<func_decl, expr*> m_right;
obj_map<expr, expr*> m_models;
bool mk_convex(expr_ref_vector const& core, unsigned index, expr_ref_vector& conv);
void mk_convex(expr* fml, unsigned index, expr_ref_vector& conv);
bool mk_convex(expr* term, unsigned index, bool is_mul, expr_ref& result);
bool translate(func_decl* fn, unsigned index, expr_ref& result);
void method1(model_node& n, expr_ref_vector& core, bool& uses_level);
void method2(model_node& n, expr_ref_vector& core, bool& uses_level);
void add_variables(model_node& n, expr_ref_vector& eqs);
public:
core_convex_hull_generalizer(context& ctx);
virtual ~core_convex_hull_generalizer() {}

2
src/muz_qe/proof_utils.cpp
View file

@ -608,3 +608,5 @@ void proof_utils::push_instantiations_up(proof_ref& pr) {
push_instantiations_up_cl push(pr.get_manager());
push(pr);
}

1
src/muz_qe/proof_utils.h
View file

@ -42,6 +42,7 @@ public:
*/
static void push_instantiations_up(proof_ref& pr);
};
#endif

39
src/muz_qe/qe_arith_plugin.cpp
View file

@ -20,7 +20,7 @@ Revision History:
#include "qe.h"
#include "ast_pp.h"
#include "expr_replacer.h"
#include "expr_safe_replace.h"
#include "bool_rewriter.h"
#include "bv_decl_plugin.h"
#include "arith_decl_plugin.h"
@ -93,7 +93,7 @@ namespace qe {
expr_ref m_one_r;
expr_ref m_tmp;
public:
scoped_ptr<expr_replacer> m_replace;
expr_safe_replace m_replace;
bool_rewriter m_bool_rewriter;
arith_rewriter m_arith_rewriter;
@ -111,7 +111,7 @@ namespace qe {
m_zero_r(m_arith.mk_numeral(numeral(0), false), m),
m_one_r(m_arith.mk_numeral(numeral(1), false), m),
m_tmp(m),
m_replace(mk_default_expr_replacer(m)),
m_replace(m),
m_bool_rewriter(m),
m_arith_rewriter(m) {
}
@ -827,7 +827,7 @@ namespace qe {
while (index <= up) {
expr* n = mk_numeral(index);
result = body;
m_replace->apply_substitution(x, n, result);
m_replace.apply_substitution(x, n, result);
ors.push_back(result);
++index;
}
@ -857,7 +857,7 @@ namespace qe {
mk_flat_and(e1, body, result);
app_ref z(m);
mk_bounded_var(up, z_bv, z);
m_replace->apply_substitution(x, z, result);
m_replace.apply_substitution(x, z, result);
}
@ -966,7 +966,7 @@ namespace qe {
<< mk_pp(e, m) << "\n";
);
expr_ref result(fml, m);
m_replace->apply_substitution(x, e, result);
m_replace.apply_substitution(x, e, result);
simplify(result);
TRACE("qe",
tout << "singular solved:\n"
@ -1044,7 +1044,7 @@ namespace qe {
tout << " = 0\n";
);
expr_ref result(fml, m);
m_replace->apply_substitution(x, p1, result);
m_replace.apply_substitution(x, p1, result);
simplify(result);
m_ctx.elim_var(index-1, result, p1);
TRACE("qe", tout << "Reduced: " << mk_pp(result, m) << "\n";);
@ -2080,7 +2080,7 @@ public:
app* atm = atoms[i];
t1 = m_util.mk_add(m_util.mk_mul(coeffs[i], z), terms[i]);
m_util.mk_divides(divisors[i], t1, new_atom);
m_util.m_replace->apply_substitution(atm, new_atom.get(), result);
m_util.m_replace.apply_substitution(atm, new_atom.get(), result);
m_ctx.add_constraint(false, mk_not(atm), new_atom);
m_ctx.add_constraint(false, mk_not(new_atom), atm);
@ -2121,7 +2121,7 @@ public:
m_util.simplify(mod_term2);
m_ctx.add_constraint(false, m.mk_eq(mod_term2, m_util.mk_zero(mod_term2)));
m_util.m_replace->apply_substitution(atm, z1, result);
m_util.m_replace.apply_substitution(atm, z1, result);
//
// conjoin (coeff*z + rest - z1) mod k == 0 to result
@ -2153,7 +2153,7 @@ public:
for (unsigned i = 0; i < sz; ++i) {
app* e = bounds.atoms(is_strict, is_lower)[i];
m_ctx.add_constraint(true, mk_not(e));
m_util.m_replace->apply_substitution(e, m.mk_false(), result);
m_util.m_replace.apply_substitution(e, m.mk_false(), result);
}
}
@ -2162,7 +2162,7 @@ public:
for (unsigned i = 0; i < sz; ++i) {
app* e = bounds.atoms(is_strict, !is_lower)[i];
m_ctx.add_constraint(true, e);
m_util.m_replace->apply_substitution(e, m.mk_true(), result);
m_util.m_replace.apply_substitution(e, m.mk_true(), result);
}
}
@ -2276,7 +2276,7 @@ public:
else {
m_ctx.add_constraint(true, e);
}
m_util.m_replace->apply_substitution(atm, m.mk_true(), result);
m_util.m_replace.apply_substitution(atm, m.mk_true(), result);
continue;
}
@ -2293,7 +2293,7 @@ public:
(same_strict && i < index);
mk_bound(result_is_strict, is_lower, a, t, b, s, tmp);
m_util.m_replace->apply_substitution(e, tmp.get(), result);
m_util.m_replace.apply_substitution(e, tmp.get(), result);
TRACE("qe",
tout << (result_is_strict?"strict result":"non-strict result") << "\n";
@ -2330,7 +2330,7 @@ public:
s = x_t.mk_term(b, s);
b = x_t.mk_coeff(b);
m_util.mk_resolve(x, strict_resolve, a, t, b, s, tmp);
m_util.m_replace->apply_substitution(e, tmp.get(), result);
m_util.m_replace.apply_substitution(e, tmp.get(), result);
m_ctx.add_constraint(true, mk_not(e), tmp);
@ -2398,7 +2398,7 @@ public:
weights_t m_weights;
th_rewriter m_rewriter;
nlarith::util m_util;
scoped_ptr<expr_replacer> m_replacer;
expr_safe_replace m_replace;
expr_ref_vector m_trail;
factor_rewriter_star m_factor_rw;
bool m_produce_models;
@ -2407,7 +2407,7 @@ public:
qe_solver_plugin(m, m.mk_family_id("arith"), ctx),
m_rewriter(m),
m_util(m),
m_replacer(mk_default_expr_replacer(m)),
m_replace(m),
m_trail(m),
m_factor_rw(m),
m_produce_models(produce_models) {
@ -2480,12 +2480,11 @@ public:
SASSERT(vl.is_unsigned());
SASSERT(vl.get_unsigned() < brs->size());
unsigned j = vl.get_unsigned();
expr_substitution sub(m);
m_replace.reset();
for (unsigned i = 0; i < brs->preds().size(); ++i) {
sub.insert(to_app(brs->preds(i)), brs->subst(j)[i]);
m_replace.insert(brs->preds(i), brs->subst(j)[i]);
}
m_replacer->set_substitution(&sub);
(*m_replacer)(fml);
m_replace(fml);
expr_ref tmp(m.mk_and(brs->constraints(j), fml), m);
m_factor_rw(tmp, fml);
if (def) {

12
src/muz_qe/qe_array_plugin.cpp
View file

@ -1,7 +1,7 @@
#include "qe.h"
#include "array_decl_plugin.h"
#include "expr_replacer.h"
#include "expr_safe_replace.h"
#include "ast_pp.h"
#include "arith_decl_plugin.h"
@ -11,13 +11,13 @@ namespace qe {
class array_plugin : public qe_solver_plugin {
scoped_ptr<expr_replacer> m_replace;
expr_safe_replace m_replace;
public:
array_plugin(i_solver_context& ctx, ast_manager& m) :
qe_solver_plugin(m, m.mk_family_id("array"), ctx),
m_replace(mk_default_expr_replacer(m))
m_replace(m)
{
}
@ -123,7 +123,7 @@ namespace qe {
if (m_ctx.is_var(a, idx) &&
!m_ctx.contains(idx)(rhs)) {
expr_ref result(fml, m);
m_replace->apply_substitution(a, rhs, result);
m_replace.apply_substitution(a, rhs, result);
m_ctx.elim_var(idx, result, rhs);
return true;
}
@ -175,7 +175,7 @@ namespace qe {
tout << "eq: " << mk_pp(lhs, m) << " == " << mk_pp(rhs, m) << "\n";
);
expr_ref result(fml, m);
m_replace->apply_substitution(A, store_B_i_t, result);
m_replace.apply_substitution(A, store_B_i_t, result);
m_ctx.add_var(B);
m_ctx.elim_var(idx, result, store_B_i_t);
return true;
@ -248,7 +248,7 @@ namespace qe {
tout << "eq: " << mk_pp(lhs, m) << " == " << mk_pp(rhs, m) << "\n";
);
expr_ref result(fml, m);
m_replace->apply_substitution(A, store_t, result);
m_replace.apply_substitution(A, store_t, result);
m_ctx.elim_var(idx, result, store_t);
return true;
}

16
src/muz_qe/qe_bool_plugin.cpp
View file

@ -25,18 +25,18 @@ Notes:
--*/
#include "qe.h"
#include "expr_replacer.h"
#include "expr_safe_replace.h"
#include "ast_pp.h"
#include "model_evaluator.h"
namespace qe {
class bool_plugin : public qe_solver_plugin {
scoped_ptr<expr_replacer> m_replace;
expr_safe_replace m_replace;
public:
bool_plugin(i_solver_context& ctx, ast_manager& m):
qe_solver_plugin(m, m.get_basic_family_id(), ctx),
m_replace(mk_default_expr_replacer(m))
m_replace(m)
{}
virtual void assign(contains_app& x, expr* fml, rational const& vl) {
@ -51,7 +51,7 @@ namespace qe {
virtual void subst(contains_app& x, rational const& vl, expr_ref& fml, expr_ref* def) {
SASSERT(vl.is_one() || vl.is_zero());
expr* tf = (vl.is_one())?m.mk_true():m.mk_false();
m_replace->apply_substitution(x.x(), tf, 0, fml);
m_replace.apply_substitution(x.x(), tf, fml);
if (def) {
*def = tf;
}
@ -103,12 +103,12 @@ namespace qe {
app* a = to_app(e);
expr* e1;
if (m_ctx.is_var(a, idx)) {
m_replace->apply_substitution(a, m.mk_true(), 0, fml);
m_replace.apply_substitution(a, m.mk_true(), fml);
m_ctx.elim_var(idx, fml, m.mk_true());
return true;
}
else if (m.is_not(e, e1) && m_ctx.is_var(e1, idx)) {
m_replace->apply_substitution(to_app(e1), m.mk_false(), 0, fml);
m_replace.apply_substitution(to_app(e1), m.mk_false(), fml);
m_ctx.elim_var(idx, fml, m.mk_false());
return true;
}
@ -148,7 +148,7 @@ namespace qe {
}
// only occurrences of 'x' must be in positive atoms
def = m.mk_true();
m_replace->apply_substitution(x, def, 0, fml);
m_replace.apply_substitution(x, def, fml);
return true;
}
else if (!p && n) {
@ -161,7 +161,7 @@ namespace qe {
if (x != *it && contains_x(*it)) return false;
}
def = m.mk_false();
m_replace->apply_substitution(x, def, 0, fml);
m_replace.apply_substitution(x, def, fml);
return true;
}
else if (contains_x(fml)) {

10
src/muz_qe/qe_bv_plugin.cpp
View file

@ -21,19 +21,19 @@ Notes:
--*/
#include "qe.h"
#include "expr_replacer.h"
#include "expr_safe_replace.h"
#include "bv_decl_plugin.h"
#include "model_evaluator.h"
namespace qe {
class bv_plugin : public qe_solver_plugin {
scoped_ptr<expr_replacer> m_replace;
bv_util m_bv;
expr_safe_replace m_replace;
bv_util m_bv;
public:
bv_plugin(i_solver_context& ctx, ast_manager& m):
qe_solver_plugin(m, m.mk_family_id("bv"), ctx),
m_replace(mk_default_expr_replacer(m)),
m_replace(m),
m_bv(m)
{}
@ -48,7 +48,7 @@ namespace qe {
virtual void subst(contains_app& x, rational const& vl, expr_ref& fml, expr_ref* def) {
app_ref c(m_bv.mk_numeral(vl, m_bv.get_bv_size(x.x())), m);
m_replace->apply_substitution(x.x(), c, 0, fml);
m_replace.apply_substitution(x.x(), c, fml);
if (def) {
*def = m_bv.mk_numeral(vl, m_bv.get_bv_size(x.x()));
}

24
src/muz_qe/qe_datatype_plugin.cpp
View file

@ -95,7 +95,7 @@
#include "qe.h"
#include "datatype_decl_plugin.h"
#include "expr_replacer.h"
#include "expr_safe_replace.h"
#include "obj_pair_hashtable.h"
#include "for_each_expr.h"
#include "ast_pp.h"
@ -415,7 +415,7 @@ namespace qe {
typedef obj_pair_map<app, func_decl, subst_clos*> subst_map;
datatype_util m_datatype_util;
scoped_ptr<expr_replacer> m_replace;
expr_safe_replace m_replace;
eqs_cache m_eqs_cache;
subst_map m_subst_cache;
ast_ref_vector m_trail;
@ -424,7 +424,7 @@ namespace qe {
datatype_plugin(i_solver_context& ctx, ast_manager& m) :
qe_solver_plugin(m, m.mk_family_id("datatype"), ctx),
m_datatype_util(m),
m_replace(mk_default_expr_replacer(m)),
m_replace(m),
m_trail(m)
{
}
@ -518,7 +518,7 @@ namespace qe {
subst_clos* sub = 0;
if (m_subst_cache.find(x.x(), c, sub)) {
m_replace->apply_substitution(x.x(), sub->first, 0, fml);
m_replace.apply_substitution(x.x(), sub->first, fml);
add_def(sub->first, def);
for (unsigned i = 0; i < sub->second.size(); ++i) {
m_ctx.add_var(sub->second[i]);
@ -541,7 +541,7 @@ namespace qe {
m_trail.push_back(t);
add_def(t, def);
m_replace->apply_substitution(x.x(), t, 0, fml);
m_replace.apply_substitution(x.x(), t, fml);
sub->first = t;
m_subst_cache.insert(x.x(), c, sub);
}
@ -673,7 +673,7 @@ namespace qe {
fml = m.mk_and(is_c, fml);
app_ref fresh_x(m.mk_fresh_const("x", s), m);
m_ctx.add_var(fresh_x);
m_replace->apply_substitution(x, fresh_x, 0, fml);
m_replace.apply_substitution(x, fresh_x, fml);
add_def(fresh_x, def);
TRACE("qe", tout << "Add recognizer " << mk_pp(is_c, m) << "\n";);
return;
@ -697,33 +697,33 @@ namespace qe {
for (unsigned i = 0; i < eqs.num_recognizers(); ++i) {
app* rec = eqs.recognizer(i);
if (rec->get_decl() == r) {
m_replace->apply_substitution(rec, m.mk_true(), fml);
m_replace.apply_substitution(rec, m.mk_true(), fml);
}
else {
m_replace->apply_substitution(rec, m.mk_false(), fml);
m_replace.apply_substitution(rec, m.mk_false(), fml);
}
}
for (unsigned i = 0; i < eqs.num_unsat(); ++i) {
m_replace->apply_substitution(eqs.unsat_atom(i), m.mk_false(), fml);
m_replace.apply_substitution(eqs.unsat_atom(i), m.mk_false(), fml);
}
if (idx < eqs.num_eqs()) {
expr* t = eqs.eq(idx);
expr* c = eqs.eq_cond(idx);
add_def(t, def);
m_replace->apply_substitution(x, t, fml);
m_replace.apply_substitution(x, t, fml);
if (!m.is_true(c)) {
fml = m.mk_and(c, fml);
}
}
else {
for (unsigned i = 0; i < eqs.num_eqs(); ++i) {
m_replace->apply_substitution(eqs.eq_atom(i), m.mk_false(), fml);
m_replace.apply_substitution(eqs.eq_atom(i), m.mk_false(), fml);
}
for (unsigned i = 0; i < eqs.num_neqs(); ++i) {
m_replace->apply_substitution(eqs.neq_atom(i), m.mk_false(), fml);
m_replace.apply_substitution(eqs.neq_atom(i), m.mk_false(), fml);
}
if (def) {
sort* s = m.get_sort(x);

14
src/muz_qe/qe_dl_plugin.cpp
View file

@ -1,6 +1,6 @@
#include "qe.h"
#include "expr_replacer.h"
#include "expr_safe_replace.h"
#include "dl_decl_plugin.h"
#include "obj_pair_hashtable.h"
#include "ast_pp.h"
@ -35,7 +35,7 @@ namespace qe {
class dl_plugin : public qe_solver_plugin {
typedef obj_pair_map<app, expr, eq_atoms*> eqs_cache;
scoped_ptr<expr_replacer> m_replace;
expr_safe_replace m_replace;
datalog::dl_decl_util m_util;
expr_ref_vector m_trail;
eqs_cache m_eqs_cache;
@ -44,7 +44,7 @@ namespace qe {
public:
dl_plugin(i_solver_context& ctx, ast_manager& m) :
qe_solver_plugin(m, m.mk_family_id("datalog_relation"), ctx),
m_replace(mk_default_expr_replacer(m)),
m_replace(m),
m_util(m),
m_trail(m)
{
@ -140,7 +140,7 @@ namespace qe {
void subst_small_domain(contains_app & x,eq_atoms& eqs, unsigned v,expr_ref & fml) {
expr_ref vl(m_util.mk_numeral(v, m.get_sort(x.x())), m);
m_replace->apply_substitution(x.x(), vl, fml);
m_replace.apply_substitution(x.x(), vl, fml);
}
// assumes that all disequalities can be satisfied.
@ -148,15 +148,15 @@ namespace qe {
SASSERT(w <= eqs.num_eqs());
if (w < eqs.num_eqs()) {
expr* e = eqs.eq(w);
m_replace->apply_substitution(x.x(), e, fml);
m_replace.apply_substitution(x.x(), e, fml);
}
else {
for (unsigned i = 0; i < eqs.num_eqs(); ++i) {
m_replace->apply_substitution(eqs.eq_atom(i), m.mk_false(), fml);
m_replace.apply_substitution(eqs.eq_atom(i), m.mk_false(), fml);
}
for (unsigned i = 0; i < eqs.num_neqs(); ++i) {
m_replace->apply_substitution(eqs.neq_atom(i), m.mk_true(), fml);
m_replace.apply_substitution(eqs.neq_atom(i), m.mk_true(), fml);
}
}
}

3
src/muz_qe/rel_context.cpp
View file

@ -75,7 +75,8 @@ namespace datalog {
};
rel_context::rel_context(context& ctx)
: m_context(ctx),
: engine_base(ctx.get_manager(), "datalog"),
m_context(ctx),
m(ctx.get_manager()),
m_rmanager(ctx),
m_answer(m),

9
src/muz_qe/rel_context.h
View file

@ -30,7 +30,7 @@ namespace datalog {
class context;
typedef vector<std::pair<func_decl*,relation_fact> > fact_vector;
class rel_context {
class rel_context : public engine_base {
context& m_context;
ast_manager& m;
relation_manager m_rmanager;
@ -59,11 +59,11 @@ namespace datalog {
context& get_context() const { return m_context; }
relation_base & get_relation(func_decl * pred);
relation_base * try_get_relation(func_decl * pred) const;
expr_ref get_last_answer() { return m_answer; }
virtual expr_ref get_answer() { return m_answer; }
bool output_profile() const;
lbool query(expr* q);
virtual lbool query(expr* q);
lbool query(unsigned num_rels, func_decl * const* rels);
void set_predicate_representation(func_decl * pred, unsigned relation_name_cnt,
@ -73,6 +73,9 @@ namespace datalog {
void set_cancel(bool f);
virtual void cancel() { set_cancel(true); }
virtual void cleanup() { set_cancel(false);}
/**
\brief Restrict the set of used predicates to \c res.

1
src/muz_qe/tab_context.cpp
View file

@ -1657,6 +1657,7 @@ namespace datalog {
};
tab::tab(context& ctx):
datalog::engine_base(ctx.get_manager(),"tabulation"),
m_imp(alloc(imp, ctx)) {
}
tab::~tab() {

17
src/muz_qe/tab_context.h
View file

@ -22,23 +22,24 @@ Revision History:
#include "ast.h"
#include "lbool.h"
#include "statistics.h"
#include "dl_util.h"
namespace datalog {
class context;
class tab {
class tab : public engine_base {
class imp;
imp* m_imp;
public:
tab(context& ctx);
~tab();
lbool query(expr* query);
void cancel();
void cleanup();
void reset_statistics();
void collect_statistics(statistics& st) const;
void display_certificate(std::ostream& out) const;
expr_ref get_answer();
virtual lbool query(expr* query);
virtual void cancel();
virtual void cleanup();
virtual void reset_statistics();
virtual void collect_statistics(statistics& st) const;
virtual void display_certificate(std::ostream& out) const;
virtual expr_ref get_answer();
};
};

18
src/nlsat/nlsat_explain.cpp
View file

@ -993,8 +993,22 @@ namespace nlsat {
}
return;
}
else if (s == -1 && !is_even) {
atom_sign = -atom_sign;
else {
// We have shown the current factor is a constant MODULO the sign of the leading coefficient (of the equation used to rewrite the factor).
if (!info.m_lc_const) {
// If the leading coefficient is not a constant, we must store this information as an extra assumption.
if (d % 2 == 0 || // d is even
is_even || // rewriting a factor of even degree, sign flip doesn't matter
_a->get_kind() == atom::EQ) { // rewriting an equation, sign flip doesn't matter
info.add_lc_diseq();
}
else {
info.add_lc_ineq();
}
}
if (s == -1 && !is_even) {
atom_sign = -atom_sign;
}
}
}
else {

12
src/shell/datalog_frontend.cpp
View file

@ -75,7 +75,7 @@ static void display_statistics(
out << "--------------\n";
out << "instructions \n";
code.display(ctx.get_rel_context(), out);
code.display(*ctx.get_rel_context(), out);
out << "--------------\n";
out << "big relations \n";
@ -83,7 +83,7 @@ static void display_statistics(
}
out << "--------------\n";
out << "relation sizes\n";
ctx.get_rel_context().get_rmanager().display_relation_sizes(out);
ctx.get_rel_context()->get_rmanager().display_relation_sizes(out);
if (verbose) {
out << "--------------\n";
@ -125,7 +125,7 @@ unsigned read_datalog(char const * file) {
params.set_sym("engine", symbol("datalog"));
datalog::context ctx(m, s_params, params);
datalog::relation_manager & rmgr = ctx.get_rel_context().get_rmanager();
datalog::relation_manager & rmgr = ctx.get_rel_context()->get_rmanager();
datalog::relation_plugin & inner_plg = *rmgr.get_relation_plugin(symbol("tr_hashtable"));
SASSERT(&inner_plg);
rmgr.register_plugin(alloc(datalog::finite_product_relation_plugin, inner_plg, rmgr));
@ -187,7 +187,7 @@ unsigned read_datalog(char const * file) {
datalog::compiler::compile(ctx, ctx.get_rules(), rules_code, termination_code);
TRACE("dl_compiler", rules_code.display(ctx.get_rel_context(), tout););
TRACE("dl_compiler", rules_code.display(*ctx.get_rel_context(), tout););
rules_code.make_annotations(ex_ctx);
@ -227,10 +227,10 @@ unsigned read_datalog(char const * file) {
TRACE("dl_compiler", ctx.display(tout);
rules_code.display(ctx.get_rel_context(), tout););
rules_code.display(*ctx.get_rel_context(), tout););
if (ctx.get_params().output_tuples()) {
ctx.get_rel_context().display_output_facts(ctx.get_rules(), std::cout);
ctx.get_rel_context()->display_output_facts(ctx.get_rules(), std::cout);
}
display_statistics(

36
src/smt/smt_model_finder.cpp
View file

@ -94,7 +94,7 @@ namespace smt {
}
obj_map<expr, unsigned> const & get_elems() const { return m_elems; }
void insert(expr * n, unsigned generation) {
if (m_elems.contains(n))
return;
@ -102,6 +102,14 @@ namespace smt {
m_elems.insert(n, generation);
SASSERT(!m_manager.is_model_value(n));
}
void remove(expr * n) {
// We can only remove n if it is in m_elems, AND m_inv was not initialized yet.
SASSERT(m_elems.contains(n));
SASSERT(m_inv.empty());
m_elems.erase(n);
m_manager.dec_ref(n);
}
void display(std::ostream & out) const {
obj_map<expr, unsigned>::iterator it = m_elems.begin();
@ -525,6 +533,30 @@ namespace smt {
}
}
// For each instantiation_set, reemove entries that do not evaluate to values.
void cleanup_instantiation_sets() {
ptr_vector<expr> to_delete;
ptr_vector<node>::const_iterator it = m_nodes.begin();
ptr_vector<node>::const_iterator end = m_nodes.end();
for (; it != end; ++it) {
node * curr = *it;
if (curr->is_root()) {
instantiation_set * s = curr->get_instantiation_set();
to_delete.reset();
obj_map<expr, unsigned> const & elems = s->get_elems();
for (obj_map<expr, unsigned>::iterator it = elems.begin(); it != elems.end(); it++) {
expr * n = it->m_key;
expr * n_val = eval(n, true);
if (!m_manager.is_value(n_val))
to_delete.push_back(n);
}
for (ptr_vector<expr>::iterator it = to_delete.begin(); it != to_delete.end(); it++) {
s->remove(*it);
}
}
}
}
void display_nodes(std::ostream & out) const {
display_key2node(out, m_uvars);
display_A_f_is(out);
@ -545,6 +577,7 @@ namespace smt {
r = 0;
else
r = tmp;
TRACE("model_finder", tout << "eval\n" << mk_pp(n, m_manager) << "\n----->\n" << mk_pp(r, m_manager) << "\n";);
m_eval_cache.insert(n, r);
m_eval_cache_range.push_back(r);
return r;
@ -1047,6 +1080,7 @@ namespace smt {
public:
void fix_model(expr_ref_vector & new_constraints) {
cleanup_instantiation_sets();
m_new_constraints = &new_constraints;
func_decl_set partial_funcs;
collect_partial_funcs(partial_funcs);

4
src/smt/theory_array_base.cpp
View file

@ -688,7 +688,7 @@ namespace smt {
}
}
}
void theory_array_base::propagate_select_to_store_parents(enode * r, enode * sel, svector<enode_pair> & todo) {
SASSERT(r->get_root() == r);
SASSERT(is_select(sel));
@ -880,7 +880,7 @@ namespace smt {
}
else {
theory_var r = mg_find(v);
void * else_val = m_else_values[r];
void * else_val = m_else_values[r];
// DISABLED. It seems wrong, since different nodes can share the same
// else_val according to the mg class.
// SASSERT(else_val == 0 || get_context().is_relevant(UNTAG(app*, else_val)));

237
src/tactic/fpa/fpa2bv_converter.cpp
View file

@ -1113,7 +1113,7 @@ void fpa2bv_converter::mk_fusedma(func_decl * f, unsigned num, expr * const * ar
mk_nzero(f, nzero);
mk_pzero(f, pzero);
mk_minus_inf(f, ninf);
mk_plus_inf(f, pinf);
mk_plus_inf(f, pinf);
expr_ref x_is_nan(m), x_is_zero(m), x_is_pos(m), x_is_neg(m), x_is_inf(m);
expr_ref y_is_nan(m), y_is_zero(m), y_is_pos(m), y_is_neg(m), y_is_inf(m);
@ -1227,6 +1227,13 @@ void fpa2bv_converter::mk_fusedma(func_decl * f, unsigned num, expr * const * ar
b_exp_ext = m_bv_util.mk_sign_extend(2, b_exp);
c_exp_ext = m_bv_util.mk_sign_extend(2, c_exp);
dbg_decouple("fpa2bv_fma_a_sig", a_sig_ext);
dbg_decouple("fpa2bv_fma_b_sig", b_sig_ext);
dbg_decouple("fpa2bv_fma_c_sig", c_sig);
dbg_decouple("fpa2bv_fma_a_exp", a_exp_ext);
dbg_decouple("fpa2bv_fma_b_exp", b_exp_ext);
dbg_decouple("fpa2bv_fma_c_exp", c_exp_ext);
expr_ref mul_sgn(m), mul_sig(m), mul_exp(m);
expr * signs[2] = { a_sgn, b_sgn };
@ -1254,6 +1261,7 @@ void fpa2bv_converter::mk_fusedma(func_decl * f, unsigned num, expr * const * ar
expr_ref swap_cond(m);
swap_cond = m_bv_util.mk_sle(mul_exp, c_exp_ext);
SASSERT(is_well_sorted(m, swap_cond));
dbg_decouple("fpa2bv_fma_swap_cond", swap_cond);
expr_ref e_sgn(m), e_sig(m), e_exp(m), f_sgn(m), f_sig(m), f_exp(m);
m_simp.mk_ite(swap_cond, c_sgn, mul_sgn, e_sgn);
@ -1270,6 +1278,11 @@ void fpa2bv_converter::mk_fusedma(func_decl * f, unsigned num, expr * const * ar
SASSERT(is_well_sorted(m, f_sig));
SASSERT(is_well_sorted(m, f_exp));
SASSERT(m_bv_util.get_bv_size(e_sig) == 2 * sbits);
SASSERT(m_bv_util.get_bv_size(f_sig) == 2 * sbits);
SASSERT(m_bv_util.get_bv_size(e_exp) == ebits + 2);
SASSERT(m_bv_util.get_bv_size(f_exp) == ebits + 2);
expr_ref res_sgn(m), res_sig(m), res_exp(m);
expr_ref exp_delta(m);
@ -1278,43 +1291,43 @@ void fpa2bv_converter::mk_fusedma(func_decl * f, unsigned num, expr * const * ar
// cap the delta
expr_ref cap(m), cap_le_delta(m);
cap = m_bv_util.mk_numeral(sbits+3, ebits+2);
cap_le_delta = m_bv_util.mk_ule(exp_delta, cap);
cap = m_bv_util.mk_numeral(2*sbits, ebits+2);
cap_le_delta = m_bv_util.mk_ule(cap, exp_delta);
m_simp.mk_ite(cap_le_delta, cap, exp_delta, exp_delta);
SASSERT(m_bv_util.get_bv_size(exp_delta) == ebits+2);
SASSERT(is_well_sorted(m, exp_delta));
dbg_decouple("fpa2bv_fma_add_exp_delta_capped", exp_delta);
// Alignment shift with sticky bit computation.
expr_ref big_f_sig(m);
big_f_sig = m_bv_util.mk_concat(f_sig, m_bv_util.mk_numeral(0, sbits+4));
SASSERT(is_well_sorted(m, big_f_sig));
// Alignment shift with sticky bit computation.
expr_ref shifted_big(m), shifted_f_sig(m), sticky_raw(m);
shifted_big = m_bv_util.mk_bv_lshr(big_f_sig, m_bv_util.mk_concat(m_bv_util.mk_numeral(0, (2*(sbits+4))-(ebits+2)), exp_delta));
shifted_f_sig = m_bv_util.mk_extract((2*(sbits+4)-1), (sbits+4), shifted_big);
SASSERT(is_well_sorted(m, shifted_f_sig));
sticky_raw = m_bv_util.mk_extract(sbits+3, 0, shifted_big);
expr_ref sticky(m), sticky_eq(m), nil_sbit4(m), one_sbit4(m);
nil_sbit4 = m_bv_util.mk_numeral(0, sbits+4);
one_sbit4 = m_bv_util.mk_numeral(1, sbits+4);
m_simp.mk_eq(sticky_raw, nil_sbit4, sticky_eq);
m_simp.mk_ite(sticky_eq, nil_sbit4, one_sbit4, sticky);
shifted_big = m_bv_util.mk_bv_lshr(
m_bv_util.mk_concat(f_sig, m_bv_util.mk_numeral(0, sbits)),
m_bv_util.mk_zero_extend((3*sbits)-(ebits+2), exp_delta));
shifted_f_sig = m_bv_util.mk_zero_extend(sbits, m_bv_util.mk_extract(3*sbits-1, 2*sbits, shifted_big));
sticky_raw = m_bv_util.mk_extract(sbits-1, 0, shifted_big);
SASSERT(m_bv_util.get_bv_size(shifted_f_sig) == 2 * sbits);
SASSERT(is_well_sorted(m, shifted_f_sig));
expr_ref sticky(m);
sticky = m_bv_util.mk_zero_extend(2*sbits-1, m.mk_app(m_bv_util.get_fid(), OP_BREDOR, sticky_raw.get()));
SASSERT(is_well_sorted(m, sticky));
dbg_decouple("fpa2bv_fma_f_sig_sticky_raw", sticky_raw);
dbg_decouple("fpa2bv_fma_f_sig_sticky", sticky);
expr * or_args[2] = { shifted_f_sig, sticky };
shifted_f_sig = m_bv_util.mk_bv_or(2, or_args);
SASSERT(is_well_sorted(m, shifted_f_sig));
expr_ref eq_sgn(m);
m_simp.mk_eq(e_sgn, f_sgn, eq_sgn);
// two extra bits for catching the overflow.
// Significant addition.
// Two extra bits for catching the overflow.
e_sig = m_bv_util.mk_zero_extend(2, e_sig);
shifted_f_sig = m_bv_util.mk_zero_extend(2, shifted_f_sig);
SASSERT(m_bv_util.get_bv_size(e_sig) == sbits+6);
SASSERT(m_bv_util.get_bv_size(shifted_f_sig) == sbits+6);
expr_ref eq_sgn(m);
m_simp.mk_eq(e_sgn, f_sgn, eq_sgn);
SASSERT(m_bv_util.get_bv_size(e_sig) == 2*sbits + 2);
SASSERT(m_bv_util.get_bv_size(shifted_f_sig) == 2*sbits + 2);
dbg_decouple("fpa2bv_fma_add_e_sig", e_sig);
dbg_decouple("fpa2bv_fma_add_shifted_f_sig", shifted_f_sig);
@ -1330,14 +1343,22 @@ void fpa2bv_converter::mk_fusedma(func_decl * f, unsigned num, expr * const * ar
dbg_decouple("fpa2bv_fma_add_sum", sum);
expr_ref sign_bv(m), n_sum(m);
sign_bv = m_bv_util.mk_extract(sbits+4, sbits+4, sum);
sign_bv = m_bv_util.mk_extract(2*sbits+1, 2*sbits+1, sum);
n_sum = m_bv_util.mk_bv_neg(sum);
expr_ref res_sig_eq(m), sig_abs(m), one_1(m);
one_1 = m_bv_util.mk_numeral(1, 1);
m_simp.mk_eq(sign_bv, one_1, res_sig_eq);
m_simp.mk_ite(res_sig_eq, n_sum, sum, sig_abs);
dbg_decouple("fpa2bv_fma_add_sign_bv", sign_bv);
dbg_decouple("fpa2bv_fma_add_n_sum", n_sum);
family_id bvfid = m_bv_util.get_fid();
dbg_decouple("fpa2bv_fma_add_sig_abs", sig_abs);
res_exp = m_bv_util.mk_bv_sub(e_exp, c_lz_ext);
// Result could overflow into 4.xxx ...
family_id bvfid = m_bv_util.get_fid();
expr_ref res_sgn_c1(m), res_sgn_c2(m), res_sgn_c3(m);
expr_ref not_e_sgn(m), not_f_sgn(m), not_sign_bv(m);
not_e_sgn = m_bv_util.mk_bv_not(e_sgn);
@ -1348,21 +1369,15 @@ void fpa2bv_converter::mk_fusedma(func_decl * f, unsigned num, expr * const * ar
res_sgn_c3 = m.mk_app(bvfid, OP_BAND, e_sgn, f_sgn);
expr * res_sgn_or_args[3] = { res_sgn_c1, res_sgn_c2, res_sgn_c3 };
res_sgn = m_bv_util.mk_bv_or(3, res_sgn_or_args);
expr_ref res_sig_eq(m), sig_abs(m), one_1(m);
one_1 = m_bv_util.mk_numeral(1, 1);
m_simp.mk_eq(sign_bv, one_1, res_sig_eq);
m_simp.mk_ite(res_sig_eq, n_sum, sum, sig_abs);
dbg_decouple("fpa2bv_fma_add_sig_abs", sig_abs);
res_sig = m_bv_util.mk_extract(sbits+3, 0, sig_abs);
res_exp = m_bv_util.mk_bv_sub(e_exp, c_lz_ext);
sticky_raw = m_bv_util.mk_extract(sbits-5, 0, sig_abs);
sticky = m_bv_util.mk_zero_extend(sbits+7, m.mk_app(bvfid, OP_BREDOR, sticky_raw.get()));
res_sig = m_bv_util.mk_extract(2*sbits-1, sbits-4, sig_abs);
SASSERT(m_bv_util.get_bv_size(res_sig) == sbits+4);
expr_ref is_zero_sig(m), nil_sbits4(m);
nil_sbits4 = m_bv_util.mk_numeral(0, sbits+4);
m_simp.mk_eq(res_sig, nil_sbits4, is_zero_sig);
SASSERT(is_well_sorted(m, is_zero_sig));
dbg_decouple("fpa2bv_fma_is_zero_sig", is_zero_sig);
@ -1390,7 +1405,151 @@ void fpa2bv_converter::mk_fusedma(func_decl * f, unsigned num, expr * const * ar
}
void fpa2bv_converter::mk_sqrt(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
NOT_IMPLEMENTED_YET();
SASSERT(num == 2);
expr_ref rm(m), x(m);
rm = args[0];
x = args[1];
expr_ref nan(m), nzero(m), pzero(m), ninf(m), pinf(m);
mk_nan(f, nan);
mk_nzero(f, nzero);
mk_pzero(f, pzero);
mk_minus_inf(f, ninf);
mk_plus_inf(f, pinf);
expr_ref x_is_nan(m), x_is_zero(m), x_is_pos(m), x_is_inf(m);
mk_is_nan(x, x_is_nan);
mk_is_zero(x, x_is_zero);
mk_is_pos(x, x_is_pos);
mk_is_inf(x, x_is_inf);
expr_ref zero1(m), one1(m);
zero1 = m_bv_util.mk_numeral(0, 1);
one1 = m_bv_util.mk_numeral(1, 1);
expr_ref c1(m), c2(m), c3(m), c4(m), c5(m), c6(m);
expr_ref v1(m), v2(m), v3(m), v4(m), v5(m), v6(m), v7(m);
// (x is NaN) -> NaN
c1 = x_is_nan;
v1 = x;
// (x is +oo) -> +oo
mk_is_pinf(x, c2);
v2 = x;
// (x is +-0) -> +-0
mk_is_zero(x, c3);
v3 = x;
// (x < 0) -> NaN
mk_is_neg(x, c4);
v4 = nan;
// else comes the actual square root.
unsigned ebits = m_util.get_ebits(f->get_range());
unsigned sbits = m_util.get_sbits(f->get_range());
SASSERT(ebits <= sbits);
expr_ref a_sgn(m), a_sig(m), a_exp(m), a_lz(m);
unpack(x, a_sgn, a_sig, a_exp, a_lz, true);
dbg_decouple("fpa2bv_sqrt_sig", a_sig);
dbg_decouple("fpa2bv_sqrt_exp", a_exp);
SASSERT(m_bv_util.get_bv_size(a_sig) == sbits);
SASSERT(m_bv_util.get_bv_size(a_exp) == ebits);
expr_ref res_sgn(m), res_sig(m), res_exp(m);
res_sgn = zero1;
expr_ref real_exp(m);
real_exp = m_bv_util.mk_bv_sub(m_bv_util.mk_sign_extend(1, a_exp), m_bv_util.mk_zero_extend(1, a_lz));
res_exp = m_bv_util.mk_sign_extend(2, m_bv_util.mk_extract(ebits, 1, real_exp));
expr_ref e_is_odd(m);
e_is_odd = m.mk_eq(m_bv_util.mk_extract(0, 0, real_exp), one1);
dbg_decouple("fpa2bv_sqrt_e_is_odd", e_is_odd);
dbg_decouple("fpa2bv_sqrt_real_exp", real_exp);
expr_ref sig_prime(m);
m_simp.mk_ite(e_is_odd, m_bv_util.mk_concat(a_sig, zero1),
m_bv_util.mk_concat(zero1, a_sig),
sig_prime);
SASSERT(m_bv_util.get_bv_size(sig_prime) == sbits+1);
dbg_decouple("fpa2bv_sqrt_sig_prime", sig_prime);
// This is algorithm 10.2 in the Handbook of Floating-Point Arithmetic
expr_ref Q(m), R(m), S(m), T(m);
const mpz & p2 = fu().fm().m_powers2(sbits+3);
Q = m_bv_util.mk_numeral(p2, sbits+5);
R = m_bv_util.mk_bv_sub(m_bv_util.mk_concat(sig_prime, m_bv_util.mk_numeral(0, 4)), Q);
S = Q;
for (unsigned i = 0; i < sbits + 3; i++) {
dbg_decouple("fpa2bv_sqrt_Q", Q);
dbg_decouple("fpa2bv_sqrt_R", R);
S = m_bv_util.mk_concat(zero1, m_bv_util.mk_extract(sbits+4, 1, S));
expr_ref twoQ_plus_S(m);
twoQ_plus_S = m_bv_util.mk_bv_add(m_bv_util.mk_concat(Q, zero1), m_bv_util.mk_concat(zero1, S));
T = m_bv_util.mk_bv_sub(m_bv_util.mk_concat(R, zero1), twoQ_plus_S);
dbg_decouple("fpa2bv_sqrt_T", T);
SASSERT(m_bv_util.get_bv_size(Q) == sbits + 5);
SASSERT(m_bv_util.get_bv_size(R) == sbits + 5);
SASSERT(m_bv_util.get_bv_size(S) == sbits + 5);
SASSERT(m_bv_util.get_bv_size(T) == sbits + 6);
expr_ref t_lt_0(m);
m_simp.mk_eq(m_bv_util.mk_extract(sbits+5, sbits+5, T), one1, t_lt_0);
expr * or_args[2] = { Q, S };
m_simp.mk_ite(t_lt_0, Q,
m_bv_util.mk_bv_or(2, or_args),
Q);
m_simp.mk_ite(t_lt_0, m_bv_util.mk_concat(m_bv_util.mk_extract(sbits+3, 0, R), zero1),
m_bv_util.mk_extract(sbits+4, 0, T),
R);
}
expr_ref is_exact(m);
m_simp.mk_eq(R, m_bv_util.mk_numeral(0, sbits+5), is_exact);
dbg_decouple("fpa2bv_sqrt_is_exact", is_exact);
expr_ref rest(m), last(m), q_is_odd(m), rest_ext(m);
last = m_bv_util.mk_extract(0, 0, Q);
rest = m_bv_util.mk_extract(sbits+3, 1, Q);
dbg_decouple("fpa2bv_sqrt_last", last);
dbg_decouple("fpa2bv_sqrt_rest", rest);
rest_ext = m_bv_util.mk_zero_extend(1, rest);
expr_ref sticky(m);
m_simp.mk_ite(is_exact, m_bv_util.mk_zero_extend(sbits+3, last),
m_bv_util.mk_numeral(1, sbits+4),
sticky);
expr * or_args[2] = { rest_ext, sticky };
res_sig = m_bv_util.mk_bv_or(2, or_args);
SASSERT(m_bv_util.get_bv_size(res_sig) == sbits + 4);
expr_ref rounded(m);
round(f->get_range(), rm, res_sgn, res_sig, res_exp, rounded);
v5 = rounded;
// And finally, we tie them together.
mk_ite(c4, v4, v5, result);
mk_ite(c3, v3, result, result);
mk_ite(c2, v2, result, result);
mk_ite(c1, v1, result, result);
SASSERT(is_well_sorted(m, result));
}
void fpa2bv_converter::mk_round_to_integral(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {

2
src/tactic/fpa/fpa2bv_rewriter.h
View file

@ -226,7 +226,7 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
bool reduce_var(var * t, expr_ref & result, proof_ref & result_pr) {
if (t->get_idx() >= m_bindings.size())
return false;
unsigned inx = m_bindings.size() - t->get_idx() - 1;
// unsigned inx = m_bindings.size() - t->get_idx() - 1;
expr_ref new_exp(m());
sort * s = t->get_sort();