mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
fixed duality bug and added some code for returning bounded status (not yet used)
This commit is contained in:
parent
e17af8a5de
commit
70a1155d71
|
@ -1152,6 +1152,13 @@ protected:
|
|||
|
||||
virtual void LearnFrom(Solver *old_solver) = 0;
|
||||
|
||||
/** Return true if the solution be incorrect due to recursion bounding.
|
||||
That is, the returned "solution" might contain all derivable facts up to the
|
||||
given recursion bound, but not be actually a fixed point.
|
||||
*/
|
||||
|
||||
virtual bool IsResultRecursionBounded() = 0;
|
||||
|
||||
virtual ~Solver(){}
|
||||
|
||||
static Solver *Create(const std::string &solver_class, RPFP *rpfp);
|
||||
|
|
|
@ -768,6 +768,29 @@ namespace Duality {
|
|||
annot.Simplify();
|
||||
}
|
||||
|
||||
bool recursionBounded;
|
||||
|
||||
/** See if the solution might be bounded. */
|
||||
void TestRecursionBounded(){
|
||||
recursionBounded = false;
|
||||
if(RecursionBound == -1)
|
||||
return;
|
||||
for(unsigned i = 0; i < nodes.size(); i++){
|
||||
Node *node = nodes[i];
|
||||
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])){
|
||||
recursionBounded = true;
|
||||
return;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
bool IsResultRecursionBounded(){
|
||||
return recursionBounded;
|
||||
}
|
||||
|
||||
/** Generate a proposed solution of the input RPFP from
|
||||
the unwinding, by unioning the instances of each node. */
|
||||
void GenSolutionFromIndSet(bool with_markers = false){
|
||||
|
@ -1026,6 +1049,7 @@ namespace Duality {
|
|||
timer_stop("ProduceCandidatesForExtension");
|
||||
if(candidates.empty()){
|
||||
GenSolutionFromIndSet();
|
||||
TestRecursionBounded();
|
||||
return true;
|
||||
}
|
||||
Candidate cand = candidates.front();
|
||||
|
|
|
@ -53,6 +53,7 @@ namespace datalog {
|
|||
MEMOUT,
|
||||
INPUT_ERROR,
|
||||
APPROX,
|
||||
BOUNDED,
|
||||
CANCELED
|
||||
};
|
||||
|
||||
|
@ -304,6 +305,8 @@ namespace datalog {
|
|||
\brief Retrieve predicates
|
||||
*/
|
||||
func_decl_set const& get_predicates() const { return m_preds; }
|
||||
ast_ref_vector const &get_pinned() const {return m_pinned; }
|
||||
|
||||
bool is_predicate(func_decl* pred) const { return m_preds.contains(pred); }
|
||||
bool is_predicate(expr * e) const { return is_app(e) && is_predicate(to_app(e)->get_decl()); }
|
||||
|
||||
|
|
|
@ -36,6 +36,7 @@ Revision History:
|
|||
#include "model_v2_pp.h"
|
||||
#include "fixedpoint_params.hpp"
|
||||
#include "used_vars.h"
|
||||
#include "func_decl_dependencies.h"
|
||||
|
||||
// template class symbol_table<family_id>;
|
||||
|
||||
|
@ -207,6 +208,46 @@ lbool dl_interface::query(::expr * query) {
|
|||
_d->rpfp->AssertAxiom(e);
|
||||
}
|
||||
|
||||
// make sure each predicate is the head of at least one clause
|
||||
func_decl_set heads;
|
||||
for(unsigned i = 0; i < clauses.size(); i++){
|
||||
expr cl = clauses[i];
|
||||
|
||||
while(true){
|
||||
if(cl.is_app()){
|
||||
decl_kind k = cl.decl().get_decl_kind();
|
||||
if(k == Implies)
|
||||
cl = cl.arg(1);
|
||||
else {
|
||||
heads.insert(cl.decl());
|
||||
break;
|
||||
}
|
||||
}
|
||||
else if(cl.is_quantifier())
|
||||
cl = cl.body();
|
||||
else break;
|
||||
}
|
||||
}
|
||||
ast_ref_vector const &pinned = m_ctx.get_pinned();
|
||||
for(unsigned i = 0; i < pinned.size(); i++){
|
||||
::ast *fa = pinned[i];
|
||||
if(is_func_decl(fa)){
|
||||
::func_decl *fd = to_func_decl(fa);
|
||||
if(m_ctx.is_predicate(fd)) {
|
||||
func_decl f(_d->ctx,fd);
|
||||
if(!heads.contains(fd)){
|
||||
int arity = f.arity();
|
||||
std::vector<expr> args;
|
||||
for(int j = 0; j < arity; j++)
|
||||
args.push_back(_d->ctx.fresh_func_decl("X",f.domain(j))());
|
||||
expr c = implies(_d->ctx.bool_val(false),f(args));
|
||||
c = _d->ctx.make_quant(Forall,args,c);
|
||||
clauses.push_back(c);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
// creates 1-1 map between clauses and rpfp edges
|
||||
_d->rpfp->FromClauses(clauses);
|
||||
|
||||
|
@ -265,7 +306,19 @@ lbool dl_interface::query(::expr * query) {
|
|||
// dealloc(rs); this is now owned by data
|
||||
|
||||
// true means the RPFP problem is SAT, so the query is UNSAT
|
||||
return ans ? l_false : l_true;
|
||||
// but we return undef if the UNSAT result is bounded
|
||||
if(ans){
|
||||
if(rs->IsResultRecursionBounded()){
|
||||
#if 0
|
||||
m_ctx.set_status(datalog::BOUNDED);
|
||||
return l_undef;
|
||||
#else
|
||||
return l_false;
|
||||
#endif
|
||||
}
|
||||
return l_false;
|
||||
}
|
||||
return l_true;
|
||||
}
|
||||
|
||||
expr_ref dl_interface::get_cover_delta(int level, ::func_decl* pred_orig) {
|
||||
|
|
|
@ -252,6 +252,11 @@ public:
|
|||
print_certificate(ctx);
|
||||
break;
|
||||
case l_undef:
|
||||
if(dlctx.get_status() == datalog::BOUNDED){
|
||||
ctx.regular_stream() << "bounded\n";
|
||||
print_certificate(ctx);
|
||||
break;
|
||||
}
|
||||
ctx.regular_stream() << "unknown\n";
|
||||
switch(dlctx.get_status()) {
|
||||
case datalog::INPUT_ERROR:
|
||||
|
|
Loading…
Reference in a new issue