mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-11 03:33:35 +00:00
Code Activity

adding recursion bounds to duality

Browse source
This commit is contained in:
Ken McMillan 2014-09-09 14:02:46 -07:00
parent 672b8e1022
commit 13b61d894c
7 changed files with 60 additions and 23 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/duality/duality.h
View file

@ -488,9 +488,10 @@ protected:
std::vector<Edge *> Incoming;
Term dual;
Node *map;
unsigned recursion_bound;
Node(const FuncDecl &_Name, const Transformer &_Annotation, const Transformer &_Bound, const Transformer &_Underapprox, const Term &_dual, RPFP *_owner, int _number)
: Name(_Name), Annotation(_Annotation), Bound(_Bound), Underapprox(_Underapprox), dual(_dual) {owner = _owner; number = _number; Outgoing = 0;}
: Name(_Name), Annotation(_Annotation), Bound(_Bound), Underapprox(_Underapprox), dual(_dual) {owner = _owner; number = _number; Outgoing = 0; recursion_bound = UINT_MAX;}
};
/** Create a node in the graph. The input is a term R(v_1...v_n)
@ -829,7 +830,7 @@ protected:
#ifdef _WINDOWS
__declspec(dllexport)
#endif
void FromClauses(const std::vector<Term> &clauses);
void FromClauses(const std::vector<Term> &clauses, const std::vector<unsigned> *bounds = 0);
void FromFixpointContext(fixedpoint fp, std::vector<Term> &queries);

5
src/duality/duality_rpfp.cpp
View file

@ -3570,7 +3570,7 @@ namespace Duality {
#define USE_QE_LITE
void RPFP::FromClauses(const std::vector<Term> &unskolemized_clauses){
void RPFP::FromClauses(const std::vector<Term> &unskolemized_clauses, const std::vector<unsigned> *bounds){
hash_map<func_decl,Node *> pmap;
func_decl fail_pred = ctx.fresh_func_decl("@Fail", ctx.bool_sort());
@ -3663,6 +3663,7 @@ namespace Duality {
pmap[R] = node;
if (is_query)
node->Bound = CreateRelation(std::vector<Term>(), ctx.bool_val(false));
node->recursion_bound = bounds ? 0 : UINT_MAX;
}
}
@ -3728,6 +3729,8 @@ namespace Duality {
Transformer T = CreateTransformer(Relparams,Indparams,body);
Edge *edge = CreateEdge(Parent,T,Children);
edge->labeled = labeled;; // remember for label extraction
if(bounds)
Parent->recursion_bound = std::max(Parent->recursion_bound,(*bounds)[i]);
// edges.push_back(edge);
}

23
src/duality/duality_solver.cpp
View file

@ -33,6 +33,7 @@ Revision History:
#include <map>
#include <list>
#include <iterator>
#include <sstream>
// TODO: make these official options or get rid of them
@ -304,7 +305,7 @@ namespace Duality {
#ifdef BOUNDED
struct Counter {
int val;
unsigned val;
Counter(){val = 0;}
};
typedef std::map<Node *,Counter> NodeToCounter;
@ -321,6 +322,10 @@ namespace Duality {
heuristic = !cex.get_tree() ? (Heuristic *)(new LocalHeuristic(rpfp))
: (Heuristic *)(new ReplayHeuristic(rpfp,cex));
#endif
// determine if we are recursion bounded
for(unsigned i = 0; i < rpfp->nodes.size(); i++)
if(rpfp->nodes[i]->recursion_bound < UINT_MAX)
RecursionBound = 0;
cex.clear(); // in case we didn't use it for heuristic
if(unwinding) delete unwinding;
unwinding = new RPFP(rpfp->ls);
@ -461,7 +466,7 @@ namespace Duality {
}
return false;
}
/** Create an instance of a node in the unwinding. Set its
annotation to true, and mark it unexpanded. */
Node* CreateNodeInstance(Node *node, int number = 0){
@ -780,10 +785,8 @@ namespace Duality {
std::vector<Node *> &insts = insts_of_node[node];
for(unsigned j = 0; j < insts.size(); j++)
if(indset->Contains(insts[j]))
if(NodePastRecursionBound(insts[j])){
if(NodePastRecursionBound(insts[j],true))
recursionBounded = true;
return;
}
}
}
@ -801,12 +804,18 @@ namespace Duality {
}
#ifdef BOUNDED
bool NodePastRecursionBound(Node *node){
bool NodePastRecursionBound(Node *node, bool report = false){
if(RecursionBound < 0) return false;
NodeToCounter &backs = back_edges[node];
for(NodeToCounter::iterator it = backs.begin(), en = backs.end(); it != en; ++it){
if(it->second.val > RecursionBound)
if(it->second.val > it->first->recursion_bound){
if(report){
std::ostringstream os;
os << "cut off " << it->first->Name.name() << " at depth " << it->second.val;
reporter->Message(os.str());
}
return true;
}
}
return false;
}

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

@ -246,6 +246,7 @@ namespace datalog {
m_rule_fmls_head = 0;
m_rule_fmls.reset();
m_rule_names.reset();
m_rule_bounds.reset();
m_argument_var_names.reset();
m_preds.reset();
m_preds_by_name.reset();
@ -474,9 +475,10 @@ namespace datalog {
return new_pred;
}
void context::add_rule(expr* rl, symbol const& name) {
void context::add_rule(expr* rl, symbol const& name, unsigned bound) {
m_rule_fmls.push_back(rl);
m_rule_names.push_back(name);
m_rule_bounds.push_back(bound);
}
void context::flush_add_rules() {
@ -1102,12 +1104,13 @@ namespace datalog {
}
}
void context::get_raw_rule_formulas(expr_ref_vector& rules, svector<symbol>& names){
void context::get_raw_rule_formulas(expr_ref_vector& rules, svector<symbol>& names, vector<unsigned> &bounds){
for (unsigned i = 0; i < m_rule_fmls.size(); ++i) {
expr_ref r = bind_variables(m_rule_fmls[i].get(), true);
rules.push_back(r.get());
// rules.push_back(m_rule_fmls[i].get());
names.push_back(m_rule_names[i]);
bounds.push_back(m_rule_bounds[i]);
}
}
@ -1125,6 +1128,7 @@ namespace datalog {
m_rule_names[i] = m_rule_names.back();
m_rule_fmls.pop_back();
m_rule_names.pop_back();
m_rule_bounds.pop_back();
--i;
}
}

5
src/muz/base/dl_context.h
View file

@ -194,6 +194,7 @@ namespace datalog {
unsigned m_rule_fmls_head;
expr_ref_vector m_rule_fmls;
svector<symbol> m_rule_names;
vector<unsigned> m_rule_bounds;
expr_ref_vector m_background;
model_converter_ref m_mc;
proof_converter_ref m_pc;
@ -366,7 +367,7 @@ namespace datalog {
rule_set & get_rules() { flush_add_rules(); return m_rule_set; }
void get_rules_as_formulas(expr_ref_vector& fmls, svector<symbol>& names);
void get_raw_rule_formulas(expr_ref_vector& fmls, svector<symbol>& names);
void get_raw_rule_formulas(expr_ref_vector& fmls, svector<symbol>& names, vector<unsigned> &bounds);
void add_fact(app * head);
void add_fact(func_decl * pred, const relation_fact & fact);
@ -383,7 +384,7 @@ namespace datalog {
/**
Method exposed from API for adding rules.
*/
void add_rule(expr* rl, symbol const& name);
void add_rule(expr* rl, symbol const& name, unsigned bound = UINT_MAX);
/**

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

@ -155,8 +155,9 @@ lbool dl_interface::query(::expr * query) {
expr_ref_vector rules(m_ctx.get_manager());
svector< ::symbol> names;
vector<unsigned> bounds;
// m_ctx.get_rules_as_formulas(rules, names);
m_ctx.get_raw_rule_formulas(rules, names);
m_ctx.get_raw_rule_formulas(rules, names, bounds);
// get all the rules as clauses
std::vector<expr> &clauses = _d->clauses;
@ -200,6 +201,7 @@ lbool dl_interface::query(::expr * query) {
expr qc = implies(q,_d->ctx.bool_val(false));
qc = _d->ctx.make_quant(Forall,b_sorts,b_names,qc);
clauses.push_back(qc);
bounds.push_back(UINT_MAX);
// get the background axioms
unsigned num_asserts = m_ctx.get_num_assertions();
@ -243,13 +245,21 @@ lbool dl_interface::query(::expr * query) {
expr c = implies(_d->ctx.bool_val(false),f(args));
c = _d->ctx.make_quant(Forall,args,c);
clauses.push_back(c);
bounds.push_back(UINT_MAX);
}
}
}
}
unsigned rb = m_ctx.get_params().recursion_bound();
std::vector<unsigned> std_bounds;
for(unsigned i = 0; i < bounds.size(); i++){
unsigned b = bounds[i];
if (b == UINT_MAX) b = rb;
std_bounds.push_back(b);
}
// creates 1-1 map between clauses and rpfp edges
_d->rpfp->FromClauses(clauses);
_d->rpfp->FromClauses(clauses,&std_bounds);
// populate the edge-to-clause map
for(unsigned i = 0; i < _d->rpfp->edges.size(); ++i)
@ -271,11 +281,12 @@ lbool dl_interface::query(::expr * query) {
rs->SetOption("stratified_inlining",m_ctx.get_params().stratified_inlining() ? "1" : "0");
rs->SetOption("batch_expand",m_ctx.get_params().batch_expand() ? "1" : "0");
rs->SetOption("conjecture_file",m_ctx.get_params().conjecture_file());
unsigned rb = m_ctx.get_params().recursion_bound();
#if 0
if(rb != UINT_MAX){
std::ostringstream os; os << rb;
rs->SetOption("recursion_bound", os.str());
}
#endif
// Solve!
bool ans;

20
src/muz/fp/dl_cmds.cpp
View file

@ -100,7 +100,7 @@ struct dl_context {
dlctx().set_predicate_representation(pred, num_kinds, kinds);
}
void add_rule(expr * rule, symbol const& name) {
void add_rule(expr * rule, symbol const& name, unsigned bound) {
init();
if (m_collected_cmds) {
expr_ref rl = m_context->bind_variables(rule, true);
@ -110,7 +110,7 @@ struct dl_context {
m_trail.push(push_back_vector<dl_context, svector<symbol> >(m_collected_cmds->m_names));
}
else {
m_context->add_rule(rule, name);
m_context->add_rule(rule, name, bound);
}
}
@ -151,19 +151,22 @@ class dl_rule_cmd : public cmd {
mutable unsigned m_arg_idx;
expr* m_t;
symbol m_name;
unsigned m_bound;
public:
dl_rule_cmd(dl_context * dl_ctx):
cmd("rule"),
m_dl_ctx(dl_ctx),
m_arg_idx(0),
m_t(0) {}
virtual char const * get_usage() const { return "(forall (q) (=> (and body) head)) :optional-name"; }
m_t(0),
m_bound(UINT_MAX) {}
virtual char const * get_usage() const { return "(forall (q) (=> (and body) head)) :optional-name :optional-recursion-bound"; }
virtual char const * get_descr(cmd_context & ctx) const { return "add a Horn rule."; }
virtual unsigned get_arity() const { return VAR_ARITY; }
virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const {
switch(m_arg_idx) {
case 0: return CPK_EXPR;
case 1: return CPK_SYMBOL;
case 2: return CPK_UINT;
default: return CPK_SYMBOL;
}
}
@ -173,13 +176,18 @@ public:
}
virtual void set_next_arg(cmd_context & ctx, symbol const & s) {
m_name = s;
m_arg_idx++;
}
virtual void set_next_arg(cmd_context & ctx, unsigned bound) {
m_bound = bound;
m_arg_idx++;
}
virtual void reset(cmd_context & ctx) { m_dl_ctx->reset(); prepare(ctx); }
virtual void prepare(cmd_context& ctx) { m_arg_idx = 0; m_name = symbol::null; }
virtual void prepare(cmd_context& ctx) { m_arg_idx = 0; m_name = symbol::null; m_bound = UINT_MAX; }
virtual void finalize(cmd_context & ctx) {
}
virtual void execute(cmd_context & ctx) {
m_dl_ctx->add_rule(m_t, m_name);
m_dl_ctx->add_rule(m_t, m_name, m_bound);
}
};