mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable
This commit is contained in:
commit
c3ee9d0f74
|
@ -26,6 +26,9 @@ Revision History:
|
|||
#include"datalog_parser.h"
|
||||
#include"cancel_eh.h"
|
||||
#include"scoped_timer.h"
|
||||
#include"dl_cmds.h"
|
||||
#include"cmd_context.h"
|
||||
#include"smt2parser.h"
|
||||
|
||||
namespace api {
|
||||
|
||||
|
@ -124,55 +127,6 @@ namespace api {
|
|||
return str.str();
|
||||
}
|
||||
|
||||
void fixedpoint_context::simplify_rules(
|
||||
unsigned num_rules, expr* const* rules,
|
||||
unsigned num_outputs, func_decl* const* outputs, expr_ref_vector& result) {
|
||||
ast_manager& m = m_context.get_manager();
|
||||
|
||||
datalog::context ctx(m, m_context.get_fparams());
|
||||
for (unsigned i = 0; i < num_rules; ++i) {
|
||||
expr* rule = rules[i], *body, *head;
|
||||
while (true) {
|
||||
if (is_quantifier(rule)) {
|
||||
rule = to_quantifier(rule)->get_expr();
|
||||
}
|
||||
else if (m.is_implies(rule, body, head)) {
|
||||
rule = head;
|
||||
}
|
||||
else {
|
||||
break;
|
||||
}
|
||||
}
|
||||
if (is_app(rule)) {
|
||||
func_decl* r = to_app(rule)->get_decl();
|
||||
if (!ctx.is_predicate(r)) {
|
||||
ctx.register_predicate(r);
|
||||
if (num_outputs == 0) {
|
||||
ctx.set_output_predicate(r);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
for (unsigned i = 0; i < num_outputs; ++i) {
|
||||
ctx.set_output_predicate(outputs[i]);
|
||||
}
|
||||
for (unsigned i = 0; i < num_rules; ++i) {
|
||||
expr* rule = rules[i];
|
||||
ctx.add_rule(rule, symbol::null);
|
||||
}
|
||||
model_converter_ref mc; // not exposed.
|
||||
proof_converter_ref pc; // not exposed.
|
||||
ctx.apply_default_transformation(mc, pc);
|
||||
datalog::rule_set const& new_rules = ctx.get_rules();
|
||||
datalog::rule_set::iterator it = new_rules.begin(), end = new_rules.end();
|
||||
for (; it != end; ++it) {
|
||||
datalog::rule* r = *it;
|
||||
expr_ref fml(m);
|
||||
r->to_formula(fml);
|
||||
result.push_back(fml);
|
||||
}
|
||||
}
|
||||
|
||||
};
|
||||
|
||||
extern "C" {
|
||||
|
@ -384,6 +338,62 @@ extern "C" {
|
|||
Z3_CATCH_RETURN("");
|
||||
}
|
||||
|
||||
Z3_ast_vector Z3_fixedpoint_from_stream(
|
||||
Z3_context c,
|
||||
Z3_fixedpoint d,
|
||||
std::istream& s) {
|
||||
ast_manager& m = mk_c(c)->m();
|
||||
dl_collected_cmds coll(m);
|
||||
cmd_context ctx(&mk_c(c)->fparams(), false, &m);
|
||||
install_dl_collect_cmds(coll, ctx);
|
||||
ctx.set_ignore_check(true);
|
||||
if (!parse_smt2_commands(ctx, s)) {
|
||||
SET_ERROR_CODE(Z3_PARSER_ERROR);
|
||||
return 0;
|
||||
}
|
||||
|
||||
Z3_ast_vector_ref* v = alloc(Z3_ast_vector_ref, m);
|
||||
mk_c(c)->save_object(v);
|
||||
for (unsigned i = 0; i < coll.m_queries.size(); ++i) {
|
||||
v->m_ast_vector.push_back(coll.m_queries[i].get());
|
||||
}
|
||||
for (unsigned i = 0; i < coll.m_rels.size(); ++i) {
|
||||
to_fixedpoint_ref(d)->ctx().register_predicate(coll.m_rels[i].get());
|
||||
}
|
||||
for (unsigned i = 0; i < coll.m_rules.size(); ++i) {
|
||||
to_fixedpoint_ref(d)->add_rule(coll.m_rules[i].get(), coll.m_names[i]);
|
||||
}
|
||||
return of_ast_vector(v);
|
||||
}
|
||||
|
||||
Z3_ast_vector Z3_API Z3_fixedpoint_from_string(
|
||||
Z3_context c,
|
||||
Z3_fixedpoint d,
|
||||
Z3_string s) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_fixedpoint_from_string(c, d, s);
|
||||
std::string str(s);
|
||||
std::istringstream is(str);
|
||||
RETURN_Z3(Z3_fixedpoint_from_stream(c, d, is));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
Z3_ast_vector Z3_API Z3_fixedpoint_from_file(
|
||||
Z3_context c,
|
||||
Z3_fixedpoint d,
|
||||
Z3_string s) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_fixedpoint_from_file(c, d, s);
|
||||
std::ifstream is(s);
|
||||
if (!is) {
|
||||
SET_ERROR_CODE(Z3_PARSER_ERROR);
|
||||
RETURN_Z3(0);
|
||||
}
|
||||
RETURN_Z3(Z3_fixedpoint_from_stream(c, d, is));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
|
||||
Z3_stats Z3_API Z3_fixedpoint_get_statistics(Z3_context c,Z3_fixedpoint d) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_fixedpoint_get_statistics(c, d);
|
||||
|
@ -419,6 +429,27 @@ extern "C" {
|
|||
Z3_CATCH;
|
||||
}
|
||||
|
||||
|
||||
Z3_ast_vector Z3_API Z3_fixedpoint_get_rules(
|
||||
Z3_context c,
|
||||
Z3_fixedpoint d)
|
||||
{
|
||||
Z3_TRY;
|
||||
LOG_Z3_fixedpoint_get_rules(c, d);
|
||||
ast_manager& m = mk_c(c)->m();
|
||||
Z3_ast_vector_ref* v = alloc(Z3_ast_vector_ref, m);
|
||||
mk_c(c)->save_object(v);
|
||||
datalog::rule_set const& rules = to_fixedpoint_ref(d)->ctx().get_rules();
|
||||
datalog::rule_set::iterator it = rules.begin(), end = rules.end();
|
||||
for (; it != end; ++it) {
|
||||
expr_ref fml(m);
|
||||
(*it)->to_formula(fml);
|
||||
v->m_ast_vector.push_back(fml);
|
||||
}
|
||||
RETURN_Z3(of_ast_vector(v));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
void Z3_API Z3_fixedpoint_set_reduce_assign_callback(
|
||||
Z3_context c, Z3_fixedpoint d, Z3_fixedpoint_reduce_assign_callback_fptr f) {
|
||||
Z3_TRY;
|
||||
|
@ -435,31 +466,6 @@ extern "C" {
|
|||
Z3_CATCH;
|
||||
}
|
||||
|
||||
Z3_ast_vector Z3_API Z3_fixedpoint_simplify_rules(
|
||||
Z3_context c,
|
||||
Z3_fixedpoint d,
|
||||
unsigned num_rules,
|
||||
Z3_ast _rules[],
|
||||
unsigned num_outputs,
|
||||
Z3_func_decl _outputs[]) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_fixedpoint_simplify_rules(c, d, num_rules, _rules, num_outputs, _outputs);
|
||||
RESET_ERROR_CODE();
|
||||
expr** rules = (expr**)_rules;
|
||||
func_decl** outputs = (func_decl**)_outputs;
|
||||
ast_manager& m = mk_c(c)->m();
|
||||
expr_ref_vector result(m);
|
||||
to_fixedpoint_ref(d)->simplify_rules(num_rules, rules, num_outputs, outputs, result);
|
||||
Z3_ast_vector_ref* v = alloc(Z3_ast_vector_ref, mk_c(c)->m());
|
||||
mk_c(c)->save_object(v);
|
||||
for (unsigned i = 0; i < result.size(); ++i) {
|
||||
v->m_ast_vector.push_back(result[i].get());
|
||||
}
|
||||
RETURN_Z3(of_ast_vector(v));
|
||||
Z3_CATCH_RETURN(0)
|
||||
}
|
||||
|
||||
|
||||
void Z3_API Z3_fixedpoint_init(Z3_context c,Z3_fixedpoint d, void* state) {
|
||||
Z3_TRY;
|
||||
// not logged
|
||||
|
|
|
@ -62,9 +62,6 @@ namespace api {
|
|||
void collect_param_descrs(param_descrs & p) { m_context.collect_params(p); }
|
||||
void updt_params(params_ref const& p) { m_context.updt_params(p); }
|
||||
|
||||
void simplify_rules(
|
||||
unsigned num_rules, expr* const* rules,
|
||||
unsigned num_outputs, func_decl* const* outputs, expr_ref_vector& result);
|
||||
};
|
||||
};
|
||||
|
||||
|
|
|
@ -261,6 +261,23 @@ namespace Microsoft.Z3
|
|||
AST.ArrayLength(queries), AST.ArrayToNative(queries));
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// Retrieve set of rules added to fixedpoint context.
|
||||
/// </summary>
|
||||
public BoolExpr[] Rules {
|
||||
get
|
||||
{
|
||||
Contract.Ensures(Contract.Result<BoolExpr[]>() != null);
|
||||
|
||||
ASTVector v = new ASTVector(Context, Native.Z3_fixedpoint_get_rules(Context.nCtx, NativeObject));
|
||||
uint n = v.Size;
|
||||
BoolExpr[] res = new BoolExpr[n];
|
||||
for (uint i = 0; i < n; i++)
|
||||
res[i] = new BoolExpr(Context, v[i].NativeObject);
|
||||
return res;
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
#region Internal
|
||||
internal Fixedpoint(Context ctx, IntPtr obj)
|
||||
|
|
|
@ -6118,7 +6118,6 @@ class Fixedpoint(Z3PPObject):
|
|||
"""Add property to predicate for the level'th unfolding. -1 is treated as infinity (infinity)"""
|
||||
Z3_fixedpoint_add_cover(self.ctx.ref(), self.fixedpoint, level, predicate.ast, property.ast)
|
||||
|
||||
|
||||
def register_relation(self, *relations):
|
||||
"""Register relation as recursive"""
|
||||
relations = _get_args(relations)
|
||||
|
@ -6135,16 +6134,35 @@ class Fixedpoint(Z3PPObject):
|
|||
args[i] = representations[i]
|
||||
Z3_fixedpoint_set_predicate_representation(self.ctx.ref(), self.fixedpoint, f.ast, sz, args)
|
||||
|
||||
def parse_string(self, s):
|
||||
"""Parse rules and queries from a string"""
|
||||
return AstVector(Z3_fixedpoint_from_string(self.ctx.ref(), self.fixedpoint, s), self.ctx)
|
||||
|
||||
def parse_file(self, f):
|
||||
"""Parse rules and queries from a file"""
|
||||
return AstVector(Z3_fixedpoint_from_file(self.ctx.ref(), self.fixedpoint, f), self.ctx)
|
||||
|
||||
def get_rules(self):
|
||||
"""retrieve rules that have been added to fixedpoint context"""
|
||||
return AstVector(Z3_fixedpoint_get_rules(self.ctx.ref(), self.fixedpoint), self.ctx)
|
||||
|
||||
def __repr__(self):
|
||||
"""Return a formatted string with all added rules and constraints."""
|
||||
return self.sexpr()
|
||||
|
||||
def sexpr(self):
|
||||
"""Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format.
|
||||
|
||||
"""Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format.
|
||||
"""
|
||||
return Z3_fixedpoint_to_string(self.ctx.ref(), self.fixedpoint, 0, (Ast * 0)())
|
||||
return Z3_fixedpoint_to_string(self.ctx.ref(), self.fixedpoint, 0, (Ast * 0)())
|
||||
|
||||
def to_string(self, queries):
|
||||
"""Return a formatted string (in Lisp-like format) with all added constraints.
|
||||
We say the string is in s-expression format.
|
||||
Include also queries.
|
||||
"""
|
||||
args, len = _to_ast_array(queries)
|
||||
return Z3_fixedpoint_to_string(self.ctx.ref(), self.fixedpoint, len, args)
|
||||
|
||||
def statistics(self):
|
||||
"""Return statistics for the last `query()`.
|
||||
"""
|
||||
|
|
|
@ -5688,19 +5688,13 @@ END_MLAPI_EXCLUDE
|
|||
__in_ecount(num_relations) Z3_symbol const relation_kinds[]);
|
||||
|
||||
/**
|
||||
\brief Simplify rules into a set of new rules that are returned.
|
||||
The simplification routines apply inlining, quantifier elimination, and other
|
||||
algebraic simplifications.
|
||||
\brief Retrieve set of rules from fixedpoint context.
|
||||
|
||||
def_API('Z3_fixedpoint_simplify_rules', AST_VECTOR, (_in(CONTEXT), _in(FIXEDPOINT), _in(UINT), _in_array(2,AST), _in(UINT), _in_array(4,FUNC_DECL)))
|
||||
*/
|
||||
Z3_ast_vector Z3_API Z3_fixedpoint_simplify_rules(
|
||||
def_API('Z3_fixedpoint_get_rules', AST_VECTOR, (_in(CONTEXT),_in(FIXEDPOINT)))
|
||||
*/
|
||||
Z3_ast_vector Z3_API Z3_fixedpoint_get_rules(
|
||||
__in Z3_context c,
|
||||
__in Z3_fixedpoint f,
|
||||
__in unsigned num_rules,
|
||||
__in_ecount(num_rules) Z3_ast rules[],
|
||||
__in unsigned num_outputs,
|
||||
__in_ecount(num_outputs) Z3_func_decl outputs[]);
|
||||
__in Z3_fixedpoint f);
|
||||
|
||||
/**
|
||||
\brief Set parameters on fixedpoint context.
|
||||
|
@ -5738,6 +5732,38 @@ END_MLAPI_EXCLUDE
|
|||
__in unsigned num_queries,
|
||||
__in_ecount(num_queries) Z3_ast queries[]);
|
||||
|
||||
/**
|
||||
\brief Parse an SMT-LIB2 string with fixedpoint rules.
|
||||
Add the rules to the current fixedpoint context.
|
||||
Return the set of queries in the file.
|
||||
|
||||
\param c - context.
|
||||
\param f - fixedpoint context.
|
||||
\param s - string containing SMT2 specification.
|
||||
|
||||
def_API('Z3_fixedpoint_from_string', AST_VECTOR, (_in(CONTEXT), _in(FIXEDPOINT), _in(STRING)))
|
||||
*/
|
||||
Z3_ast_vector Z3_API Z3_fixedpoint_from_string(
|
||||
__in Z3_context c,
|
||||
__in Z3_fixedpoint f,
|
||||
__in Z3_string s);
|
||||
|
||||
/**
|
||||
\brief Parse an SMT-LIB2 file with fixedpoint rules.
|
||||
Add the rules to the current fixedpoint context.
|
||||
Return the set of queries in the file.
|
||||
|
||||
\param c - context.
|
||||
\param f - fixedpoint context.
|
||||
\param s - string containing SMT2 specification.
|
||||
|
||||
def_API('Z3_fixedpoint_from_file', AST_VECTOR, (_in(CONTEXT), _in(FIXEDPOINT), _in(STRING)))
|
||||
*/
|
||||
Z3_ast_vector Z3_API Z3_fixedpoint_from_file(
|
||||
__in Z3_context c,
|
||||
__in Z3_fixedpoint f,
|
||||
__in Z3_string s);
|
||||
|
||||
/**
|
||||
\brief Create a backtracking point.
|
||||
|
||||
|
|
|
@ -317,8 +317,8 @@ class smt_printer {
|
|||
}
|
||||
|
||||
void visit_sort(sort* s, bool bool2int = false) {
|
||||
symbol sym;
|
||||
if (bool2int && is_bool(s)) {
|
||||
symbol sym;
|
||||
if (bool2int && is_bool(s) && !m_is_smt2) {
|
||||
sym = symbol("Int");
|
||||
} else if (s->is_sort_of(m_bv_fid, BV_SORT)) {
|
||||
sym = symbol("BitVec");
|
||||
|
|
|
@ -6,8 +6,9 @@
|
|||
#include "arith_decl_plugin.h"
|
||||
#include "front_end_params.h"
|
||||
#include "th_rewriter.h"
|
||||
#include "var_subst.h"
|
||||
|
||||
#define IS_EQUIV(_e_) (m_manager.is_eq(_e_) || m_manager.is_iff(_e_))
|
||||
#define IS_EQUIV(_e_) (m.is_eq(_e_) || m.is_iff(_e_))
|
||||
|
||||
#define SAME_OP(_d1_, _d2_) ((_d1_ == _d2_) || (IS_EQUIV(_d1_) && IS_EQUIV(_d2_)))
|
||||
|
||||
|
@ -79,7 +80,7 @@ void proof_checker::hyp_decl_plugin::get_sort_names(svector<builtin_name> & sort
|
|||
}
|
||||
}
|
||||
|
||||
proof_checker::proof_checker(ast_manager& m) : m_manager(m), m_todo(m), m_marked(), m_pinned(m), m_nil(m),
|
||||
proof_checker::proof_checker(ast_manager& m) : m(m), m_todo(m), m_marked(), m_pinned(m), m_nil(m),
|
||||
m_dump_lemmas(false), m_logic("AUFLIA"), m_proof_lemma_id(0) {
|
||||
symbol fam_name("proof_hypothesis");
|
||||
if (!m.has_plugin(fam_name)) {
|
||||
|
@ -87,11 +88,11 @@ proof_checker::proof_checker(ast_manager& m) : m_manager(m), m_todo(m), m_marked
|
|||
}
|
||||
m_hyp_fid = m.get_family_id(fam_name);
|
||||
// m_spc_fid = m.get_family_id("spc");
|
||||
m_nil = m_manager.mk_const(m_hyp_fid, OP_NIL);
|
||||
m_nil = m.mk_const(m_hyp_fid, OP_NIL);
|
||||
}
|
||||
|
||||
bool proof_checker::check(proof* p, expr_ref_vector& side_conditions) {
|
||||
proof_ref curr(m_manager);
|
||||
proof_ref curr(m);
|
||||
m_todo.push_back(p);
|
||||
|
||||
bool result = true;
|
||||
|
@ -100,7 +101,7 @@ bool proof_checker::check(proof* p, expr_ref_vector& side_conditions) {
|
|||
m_todo.pop_back();
|
||||
result = check1(curr.get(), side_conditions);
|
||||
if (!result) {
|
||||
IF_VERBOSE(0, ast_ll_pp(verbose_stream() << "Proof check failed\n", m_manager, curr.get()););
|
||||
IF_VERBOSE(0, ast_ll_pp(verbose_stream() << "Proof check failed\n", m, curr.get()););
|
||||
UNREACHABLE();
|
||||
}
|
||||
}
|
||||
|
@ -114,7 +115,7 @@ bool proof_checker::check(proof* p, expr_ref_vector& side_conditions) {
|
|||
}
|
||||
|
||||
bool proof_checker::check1(proof* p, expr_ref_vector& side_conditions) {
|
||||
if (p->get_family_id() == m_manager.get_basic_family_id()) {
|
||||
if (p->get_family_id() == m.get_basic_family_id()) {
|
||||
return check1_basic(p, side_conditions);
|
||||
}
|
||||
#if 0
|
||||
|
@ -129,11 +130,11 @@ bool proof_checker::check1_spc(proof* p, expr_ref_vector& side_conditions) {
|
|||
#if 0
|
||||
decl_kind k = p->get_decl_kind();
|
||||
bool is_univ = false;
|
||||
expr_ref fact(m_manager), fml(m_manager);
|
||||
expr_ref body(m_manager), fml1(m_manager), fml2(m_manager);
|
||||
sort_ref_vector sorts(m_manager);
|
||||
proof_ref p1(m_manager), p2(m_manager);
|
||||
proof_ref_vector proofs(m_manager);
|
||||
expr_ref fact(m), fml(m);
|
||||
expr_ref body(m), fml1(m), fml2(m);
|
||||
sort_ref_vector sorts(m);
|
||||
proof_ref p1(m), p2(m);
|
||||
proof_ref_vector proofs(m);
|
||||
|
||||
if (match_proof(p, proofs)) {
|
||||
for (unsigned i = 0; i < proofs.size(); ++i) {
|
||||
|
@ -159,15 +160,15 @@ bool proof_checker::check1_spc(proof* p, expr_ref_vector& side_conditions) {
|
|||
case PR_FACTORING:
|
||||
case PR_SPC_DER: {
|
||||
if (match_fact(p, fact)) {
|
||||
expr_ref_vector rewrite_eq(m_manager);
|
||||
expr_ref_vector rewrite_eq(m);
|
||||
rewrite_eq.push_back(fact.get());
|
||||
for (unsigned i = 0; i < proofs.size(); ++i) {
|
||||
if (match_fact(proofs[i].get(), fml)) {
|
||||
rewrite_eq.push_back(m_manager.mk_not(fml.get()));
|
||||
rewrite_eq.push_back(m.mk_not(fml.get()));
|
||||
}
|
||||
}
|
||||
expr_ref rewrite_cond(m_manager);
|
||||
rewrite_cond = m_manager.mk_or(rewrite_eq.size(), rewrite_eq.c_ptr());
|
||||
expr_ref rewrite_cond(m);
|
||||
rewrite_cond = m.mk_or(rewrite_eq.size(), rewrite_eq.c_ptr());
|
||||
side_conditions.push_back(rewrite_cond.get());
|
||||
return true;
|
||||
}
|
||||
|
@ -184,18 +185,18 @@ bool proof_checker::check1_spc(proof* p, expr_ref_vector& side_conditions) {
|
|||
|
||||
bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
|
||||
decl_kind k = p->get_decl_kind();
|
||||
expr_ref fml0(m_manager), fml1(m_manager), fml2(m_manager), fml(m_manager);
|
||||
expr_ref t1(m_manager), t2(m_manager);
|
||||
expr_ref s1(m_manager), s2(m_manager);
|
||||
expr_ref u1(m_manager), u2(m_manager);
|
||||
expr_ref fact(m_manager), body1(m_manager), body2(m_manager);
|
||||
expr_ref l1(m_manager), l2(m_manager), r1(m_manager), r2(m_manager);
|
||||
func_decl_ref d1(m_manager), d2(m_manager), d3(m_manager);
|
||||
proof_ref p0(m_manager), p1(m_manager), p2(m_manager);
|
||||
proof_ref_vector proofs(m_manager);
|
||||
func_decl_ref f1(m_manager), f2(m_manager);
|
||||
expr_ref_vector terms1(m_manager), terms2(m_manager), terms(m_manager);
|
||||
sort_ref_vector decls1(m_manager), decls2(m_manager);
|
||||
expr_ref fml0(m), fml1(m), fml2(m), fml(m);
|
||||
expr_ref t1(m), t2(m);
|
||||
expr_ref s1(m), s2(m);
|
||||
expr_ref u1(m), u2(m);
|
||||
expr_ref fact(m), body1(m), body2(m);
|
||||
expr_ref l1(m), l2(m), r1(m), r2(m);
|
||||
func_decl_ref d1(m), d2(m), d3(m);
|
||||
proof_ref p0(m), p1(m), p2(m);
|
||||
proof_ref_vector proofs(m);
|
||||
func_decl_ref f1(m), f2(m);
|
||||
expr_ref_vector terms1(m), terms2(m), terms(m);
|
||||
sort_ref_vector decls1(m), decls2(m);
|
||||
|
||||
if (match_proof(p, proofs)) {
|
||||
for (unsigned i = 0; i < proofs.size(); ++i) {
|
||||
|
@ -296,7 +297,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
|
|||
return false;
|
||||
}
|
||||
case PR_MONOTONICITY: {
|
||||
TRACE("proof_checker", tout << mk_bounded_pp(p, m_manager, 3) << "\n";);
|
||||
TRACE("proof_checker", tout << mk_bounded_pp(p, m, 3) << "\n";);
|
||||
if (match_fact(p, fact) &&
|
||||
match_binary(fact.get(), d1, t1, t2) &&
|
||||
match_app(t1.get(), f1, terms1) &&
|
||||
|
@ -334,7 +335,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
|
|||
match_fact(p1.get(), fml) &&
|
||||
(match_iff(fact.get(), t1, t2) || match_oeq(fact.get(), t1, t2)) &&
|
||||
(match_iff(fml.get(), s1, s2) || match_oeq(fml.get(), s1, s2)) &&
|
||||
m_manager.is_oeq(fact.get()) == m_manager.is_oeq(fml.get()) &&
|
||||
m.is_oeq(fact.get()) == m.is_oeq(fml.get()) &&
|
||||
is_quantifier(t1.get()) &&
|
||||
is_quantifier(t2.get()) &&
|
||||
to_quantifier(t1.get())->get_expr() == s1.get() &&
|
||||
|
@ -366,7 +367,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
|
|||
return false;
|
||||
}
|
||||
case PR_AND_ELIM: {
|
||||
expr_ref_vector terms(m_manager);
|
||||
expr_ref_vector terms(m);
|
||||
if (match_proof(p, p1) &&
|
||||
match_fact(p, fact) &&
|
||||
match_fact(p1.get(), fml) &&
|
||||
|
@ -381,7 +382,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
|
|||
return false;
|
||||
}
|
||||
case PR_NOT_OR_ELIM: {
|
||||
expr_ref_vector terms(m_manager);
|
||||
expr_ref_vector terms(m);
|
||||
if (match_proof(p, p1) &&
|
||||
match_fact(p, fact) &&
|
||||
match_fact(p1.get(), fml) &&
|
||||
|
@ -403,25 +404,25 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
|
|||
side_conditions.push_back(fact.get());
|
||||
return true;
|
||||
}
|
||||
IF_VERBOSE(0, verbose_stream() << "Expected proof of equality:\n" << mk_bounded_pp(p, m_manager););
|
||||
IF_VERBOSE(0, verbose_stream() << "Expected proof of equality:\n" << mk_bounded_pp(p, m););
|
||||
return false;
|
||||
}
|
||||
case PR_REWRITE_STAR: {
|
||||
if (match_fact(p, fact) &&
|
||||
match_equiv(fact.get(), t1, t2)) {
|
||||
expr_ref_vector rewrite_eq(m_manager);
|
||||
expr_ref_vector rewrite_eq(m);
|
||||
rewrite_eq.push_back(fact.get());
|
||||
for (unsigned i = 0; i < proofs.size(); ++i) {
|
||||
if (match_fact(proofs[i].get(), fml)) {
|
||||
rewrite_eq.push_back(m_manager.mk_not(fml.get()));
|
||||
rewrite_eq.push_back(m.mk_not(fml.get()));
|
||||
}
|
||||
}
|
||||
expr_ref rewrite_cond(m_manager);
|
||||
rewrite_cond = m_manager.mk_or(rewrite_eq.size(), rewrite_eq.c_ptr());
|
||||
expr_ref rewrite_cond(m);
|
||||
rewrite_cond = m.mk_or(rewrite_eq.size(), rewrite_eq.c_ptr());
|
||||
side_conditions.push_back(rewrite_cond.get());
|
||||
return true;
|
||||
}
|
||||
IF_VERBOSE(0, verbose_stream() << "Expected proof of equality:\n" << mk_bounded_pp(p, m_manager););
|
||||
IF_VERBOSE(0, verbose_stream() << "Expected proof of equality:\n" << mk_bounded_pp(p, m););
|
||||
return false;
|
||||
}
|
||||
case PR_PULL_QUANT: {
|
||||
|
@ -432,7 +433,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
|
|||
// TBD: check the enchilada.
|
||||
return true;
|
||||
}
|
||||
IF_VERBOSE(0, verbose_stream() << "Expected proof of equivalence with a quantifier:\n" << mk_bounded_pp(p, m_manager););
|
||||
IF_VERBOSE(0, verbose_stream() << "Expected proof of equivalence with a quantifier:\n" << mk_bounded_pp(p, m););
|
||||
return false;
|
||||
}
|
||||
case PR_PULL_QUANT_STAR: {
|
||||
|
@ -442,7 +443,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
|
|||
// TBD: check the enchilada.
|
||||
return true;
|
||||
}
|
||||
IF_VERBOSE(0, verbose_stream() << "Expected proof of equivalence:\n" << mk_bounded_pp(p, m_manager););
|
||||
IF_VERBOSE(0, verbose_stream() << "Expected proof of equivalence:\n" << mk_bounded_pp(p, m););
|
||||
return false;
|
||||
}
|
||||
case PR_PUSH_QUANT: {
|
||||
|
@ -509,9 +510,9 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
|
|||
if (match_proof(p, p1) &&
|
||||
match_fact(p, fact) &&
|
||||
match_fact(p1.get(), fml) &&
|
||||
m_manager.is_false(fml.get())) {
|
||||
expr_ref_vector hypotheses(m_manager);
|
||||
expr_ref_vector ors(m_manager);
|
||||
m.is_false(fml.get())) {
|
||||
expr_ref_vector hypotheses(m);
|
||||
expr_ref_vector ors(m);
|
||||
get_hypotheses(p1.get(), hypotheses);
|
||||
if (hypotheses.size() == 1 && match_negated(hypotheses.get(0), fact)) {
|
||||
// Suppose fact is (or a b c) and hypothesis is (not (or a b c))
|
||||
|
@ -531,18 +532,18 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
|
|||
tout << "i: " << i << "\n";
|
||||
tout << "ORs:\n";
|
||||
for (unsigned i = 0; i < ors.size(); i++) {
|
||||
tout << mk_pp(ors.get(i), m_manager) << "\n";
|
||||
tout << mk_pp(ors.get(i), m) << "\n";
|
||||
}
|
||||
tout << "HYPOTHESIS:\n";
|
||||
for (unsigned i = 0; i < hypotheses.size(); i++) {
|
||||
tout << mk_pp(hypotheses.get(i), m_manager) << "\n";
|
||||
tout << mk_pp(hypotheses.get(i), m) << "\n";
|
||||
});
|
||||
UNREACHABLE();
|
||||
return false;
|
||||
}
|
||||
TRACE("proof_checker", tout << "Matched:\n";
|
||||
ast_ll_pp(tout, m_manager, hypotheses[i].get());
|
||||
ast_ll_pp(tout, m_manager, ors[j-1].get()););
|
||||
ast_ll_pp(tout, m, hypotheses[i].get());
|
||||
ast_ll_pp(tout, m, ors[j-1].get()););
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
@ -555,7 +556,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
|
|||
match_fact(proofs[0].get(), fml1) &&
|
||||
match_fact(proofs[1].get(), fml2) &&
|
||||
match_negated(fml1.get(), fml2.get()) &&
|
||||
m_manager.is_false(fact.get())) {
|
||||
m.is_false(fact.get())) {
|
||||
return true;
|
||||
}
|
||||
if (match_fact(p, fact) &&
|
||||
|
@ -580,15 +581,15 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
|
|||
TRACE("pr_unit_bug",
|
||||
tout << "Parents:\n";
|
||||
for (unsigned i = 0; i < proofs.size(); i++) {
|
||||
expr_ref p(m_manager);
|
||||
expr_ref p(m);
|
||||
match_fact(proofs.get(i), p);
|
||||
tout << mk_pp(p, m_manager) << "\n";
|
||||
tout << mk_pp(p, m) << "\n";
|
||||
}
|
||||
tout << "Fact:\n";
|
||||
tout << mk_pp(fact, m_manager) << "\n";
|
||||
tout << mk_pp(fact, m) << "\n";
|
||||
tout << "Clause:\n";
|
||||
tout << mk_pp(fml, m_manager) << "\n";
|
||||
tout << "Could not find premise " << mk_pp(fml2, m_manager) << "\n";
|
||||
tout << mk_pp(fml, m) << "\n";
|
||||
tout << "Could not find premise " << mk_pp(fml2, m) << "\n";
|
||||
);
|
||||
|
||||
UNREACHABLE();
|
||||
|
@ -597,7 +598,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
|
|||
}
|
||||
switch(terms1.size()) {
|
||||
case 0:
|
||||
return m_manager.is_false(fact.get());
|
||||
return m.is_false(fact.get());
|
||||
case 1:
|
||||
return fact.get() == terms1[0].get();
|
||||
default: {
|
||||
|
@ -609,15 +610,15 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
|
|||
found = term1 == terms2[j].get();
|
||||
}
|
||||
if (!found) {
|
||||
IF_VERBOSE(0, verbose_stream() << "Premise not found:" << mk_pp(term1, m_manager) << "\n";);
|
||||
IF_VERBOSE(0, verbose_stream() << "Premise not found:" << mk_pp(term1, m) << "\n";);
|
||||
return false;
|
||||
}
|
||||
}
|
||||
return true;
|
||||
}
|
||||
IF_VERBOSE(0, verbose_stream() << "Conclusion is not a disjunction:\n";
|
||||
verbose_stream() << mk_pp(fml.get(), m_manager) << "\n";
|
||||
verbose_stream() << mk_pp(fact.get(), m_manager) << "\n";);
|
||||
verbose_stream() << mk_pp(fml.get(), m) << "\n";
|
||||
verbose_stream() << mk_pp(fact.get(), m) << "\n";);
|
||||
|
||||
return false;
|
||||
}
|
||||
|
@ -634,7 +635,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
|
|||
match_fact(p1.get(), fml1) &&
|
||||
match_iff(fact.get(), l1, r1) &&
|
||||
fml1.get() == l1.get() &&
|
||||
r1.get() == m_manager.mk_true()) {
|
||||
r1.get() == m.mk_true()) {
|
||||
return true;
|
||||
}
|
||||
UNREACHABLE();
|
||||
|
@ -648,7 +649,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
|
|||
match_iff(fact.get(), l1, r1) &&
|
||||
match_not(fml1.get(), t1) &&
|
||||
t1.get() == l1.get() &&
|
||||
r1.get() == m_manager.mk_false()) {
|
||||
r1.get() == m.mk_false()) {
|
||||
return true;
|
||||
}
|
||||
UNREACHABLE();
|
||||
|
@ -674,7 +675,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
|
|||
// axiom(?fml)
|
||||
if (match_fact(p, fact) &&
|
||||
match_proof(p) &&
|
||||
m_manager.is_bool(fact.get())) {
|
||||
m.is_bool(fact.get())) {
|
||||
return true;
|
||||
}
|
||||
UNREACHABLE();
|
||||
|
@ -689,7 +690,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
|
|||
//
|
||||
if (match_fact(p, fact) &&
|
||||
match_proof(p) &&
|
||||
m_manager.is_bool(fact.get())) {
|
||||
m.is_bool(fact.get())) {
|
||||
return true;
|
||||
}
|
||||
UNREACHABLE();
|
||||
|
@ -790,16 +791,138 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
|
|||
// TODO
|
||||
return true;
|
||||
}
|
||||
case PR_HYPER_RESOLVE: {
|
||||
proof_ref_vector premises(m);
|
||||
expr_ref_vector fmls(m);
|
||||
expr_ref conclusion(m), premise(m), premise0(m), premise1(m);
|
||||
svector<std::pair<unsigned, unsigned> > positions;
|
||||
vector<expr_ref_vector> substs;
|
||||
VERIFY(m.is_hyper_resolve(p, premises, conclusion, positions, substs));
|
||||
var_subst vs(m, false);
|
||||
for (unsigned i = 0; i < premises.size(); ++i) {
|
||||
expr_ref_vector const& sub = substs[i];
|
||||
premise = m.get_fact(premises[i].get());
|
||||
if (!sub.empty()) {
|
||||
if (is_forall(premise)) {
|
||||
// SASSERT(to_quantifier(premise)->get_num_decls() == sub.size());
|
||||
premise = to_quantifier(premise)->get_expr();
|
||||
}
|
||||
vs(premise, sub.size(), sub.c_ptr(), premise);
|
||||
}
|
||||
fmls.push_back(premise.get());
|
||||
TRACE("proof_checker",
|
||||
tout << mk_pp(premise.get(), m) << "\n";
|
||||
for (unsigned j = 0; j < sub.size(); ++j) {
|
||||
tout << mk_pp(sub[j], m) << " ";
|
||||
}
|
||||
tout << "\n";);
|
||||
}
|
||||
premise0 = fmls[0].get();
|
||||
for (unsigned i = 1; i < fmls.size(); ++i) {
|
||||
expr_ref lit1(m), lit2(m);
|
||||
expr* lit3 = 0;
|
||||
std::pair<unsigned, unsigned> pos = positions[i-1];
|
||||
premise1 = fmls[i].get();
|
||||
set_false(premise0, pos.first, lit1);
|
||||
set_false(premise1, pos.second, lit2);
|
||||
if (m.is_not(lit1, lit3) && lit3 == lit2) {
|
||||
// ok
|
||||
}
|
||||
else if (m.is_not(lit2, lit3) && lit3 == lit1) {
|
||||
// ok
|
||||
}
|
||||
else {
|
||||
IF_VERBOSE(0, verbose_stream() << "Could not establish complementarity for:\n" <<
|
||||
mk_pp(lit1, m) << "\n" << mk_pp(lit2, m) << "\n";);
|
||||
}
|
||||
fmls[i] = premise1;
|
||||
}
|
||||
fmls[0] = premise0;
|
||||
premise0 = m.mk_or(fmls.size(), fmls.c_ptr());
|
||||
if (is_forall(conclusion)) {
|
||||
quantifier* q = to_quantifier(conclusion);
|
||||
premise0 = m.mk_iff(premise0, q->get_expr());
|
||||
premise0 = m.mk_forall(q->get_num_decls(), q->get_decl_sorts(), q->get_decl_names(), premise0);
|
||||
}
|
||||
else {
|
||||
premise0 = m.mk_iff(premise0, conclusion);
|
||||
}
|
||||
side_conditions.push_back(premise0);
|
||||
return true;
|
||||
}
|
||||
default:
|
||||
UNREACHABLE();
|
||||
return false;
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Premises of the rules are of the form
|
||||
(or l0 l1 l2 .. ln)
|
||||
or
|
||||
(=> (and ln+1 ln+2 .. ln+m) l0)
|
||||
or in the most general (ground) form:
|
||||
(=> (and ln+1 ln+2 .. ln+m) (or l0 l1 .. ln-1))
|
||||
In other words we use the following (Prolog style) convention for Horn
|
||||
implications:
|
||||
The head of a Horn implication is position 0,
|
||||
the first conjunct in the body of an implication is position 1
|
||||
the second conjunct in the body of an implication is position 2
|
||||
|
||||
Set the position provided in the argument to 'false'.
|
||||
*/
|
||||
void proof_checker::set_false(expr_ref& e, unsigned position, expr_ref& lit) {
|
||||
app* a = to_app(e);
|
||||
expr* head, *body;
|
||||
expr_ref_vector args(m);
|
||||
if (m.is_or(e)) {
|
||||
SASSERT(position < a->get_num_args());
|
||||
args.append(a->get_num_args(), a->get_args());
|
||||
lit = args[position].get();
|
||||
args[position] = m.mk_false();
|
||||
e = m.mk_or(args.size(), args.c_ptr());
|
||||
}
|
||||
else if (m.is_implies(e, body, head)) {
|
||||
expr* const* heads = &head;
|
||||
unsigned num_heads = 1;
|
||||
if (m.is_or(head)) {
|
||||
num_heads = to_app(head)->get_num_args();
|
||||
heads = to_app(head)->get_args();
|
||||
}
|
||||
expr*const* bodies = &body;
|
||||
unsigned num_bodies = 1;
|
||||
if (m.is_and(body)) {
|
||||
num_bodies = to_app(body)->get_num_args();
|
||||
bodies = to_app(body)->get_args();
|
||||
}
|
||||
if (position < num_heads) {
|
||||
args.append(num_heads, heads);
|
||||
lit = args[position].get();
|
||||
args[position] = m.mk_false();
|
||||
e = m.mk_implies(body, m.mk_or(args.size(), args.c_ptr()));
|
||||
}
|
||||
else {
|
||||
position -= num_heads;
|
||||
args.append(num_bodies, bodies);
|
||||
lit = m.mk_not(args[position].get());
|
||||
args[position] = m.mk_true();
|
||||
e = m.mk_implies(m.mk_and(args.size(), args.c_ptr()), head);
|
||||
}
|
||||
}
|
||||
else if (position == 0) {
|
||||
lit = e;
|
||||
e = m.mk_false();
|
||||
}
|
||||
else {
|
||||
IF_VERBOSE(0, verbose_stream() << position << "\n" << mk_pp(e, m) << "\n";);
|
||||
UNREACHABLE();
|
||||
}
|
||||
}
|
||||
|
||||
bool proof_checker::match_fact(proof* p, expr_ref& fact) {
|
||||
if (m_manager.is_proof(p) &&
|
||||
m_manager.has_fact(p)) {
|
||||
fact = m_manager.get_fact(p);
|
||||
if (m.is_proof(p) &&
|
||||
m.has_fact(p)) {
|
||||
fact = m.get_fact(p);
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
|
@ -814,33 +937,33 @@ void proof_checker::add_premise(proof* p) {
|
|||
|
||||
bool proof_checker::match_proof(proof* p) {
|
||||
return
|
||||
m_manager.is_proof(p) &&
|
||||
m_manager.get_num_parents(p) == 0;
|
||||
m.is_proof(p) &&
|
||||
m.get_num_parents(p) == 0;
|
||||
}
|
||||
|
||||
bool proof_checker::match_proof(proof* p, proof_ref& p0) {
|
||||
if (m_manager.is_proof(p) &&
|
||||
m_manager.get_num_parents(p) == 1) {
|
||||
p0 = m_manager.get_parent(p, 0);
|
||||
if (m.is_proof(p) &&
|
||||
m.get_num_parents(p) == 1) {
|
||||
p0 = m.get_parent(p, 0);
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
bool proof_checker::match_proof(proof* p, proof_ref& p0, proof_ref& p1) {
|
||||
if (m_manager.is_proof(p) &&
|
||||
m_manager.get_num_parents(p) == 2) {
|
||||
p0 = m_manager.get_parent(p, 0);
|
||||
p1 = m_manager.get_parent(p, 1);
|
||||
if (m.is_proof(p) &&
|
||||
m.get_num_parents(p) == 2) {
|
||||
p0 = m.get_parent(p, 0);
|
||||
p1 = m.get_parent(p, 1);
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
bool proof_checker::match_proof(proof* p, proof_ref_vector& parents) {
|
||||
if (m_manager.is_proof(p)) {
|
||||
for (unsigned i = 0; i < m_manager.get_num_parents(p); ++i) {
|
||||
parents.push_back(m_manager.get_parent(p, i));
|
||||
if (m.is_proof(p)) {
|
||||
for (unsigned i = 0; i < m.get_num_parents(p); ++i) {
|
||||
parents.push_back(m.get_parent(p, i));
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
@ -886,7 +1009,7 @@ bool proof_checker::match_quantifier(expr* e, bool& is_univ, sort_ref_vector& so
|
|||
|
||||
bool proof_checker::match_op(expr* e, decl_kind k, expr_ref& t1, expr_ref& t2) {
|
||||
if (e->get_kind() == AST_APP &&
|
||||
to_app(e)->get_family_id() == m_manager.get_basic_family_id() &&
|
||||
to_app(e)->get_family_id() == m.get_basic_family_id() &&
|
||||
to_app(e)->get_decl_kind() == k &&
|
||||
to_app(e)->get_num_args() == 2) {
|
||||
t1 = to_app(e)->get_arg(0);
|
||||
|
@ -898,7 +1021,7 @@ bool proof_checker::match_op(expr* e, decl_kind k, expr_ref& t1, expr_ref& t2) {
|
|||
|
||||
bool proof_checker::match_op(expr* e, decl_kind k, expr_ref_vector& terms) {
|
||||
if (e->get_kind() == AST_APP &&
|
||||
to_app(e)->get_family_id() == m_manager.get_basic_family_id() &&
|
||||
to_app(e)->get_family_id() == m.get_basic_family_id() &&
|
||||
to_app(e)->get_decl_kind() == k) {
|
||||
for (unsigned i = 0; i < to_app(e)->get_num_args(); ++i) {
|
||||
terms.push_back(to_app(e)->get_arg(i));
|
||||
|
@ -911,7 +1034,7 @@ bool proof_checker::match_op(expr* e, decl_kind k, expr_ref_vector& terms) {
|
|||
|
||||
bool proof_checker::match_op(expr* e, decl_kind k, expr_ref& t) {
|
||||
if (e->get_kind() == AST_APP &&
|
||||
to_app(e)->get_family_id() == m_manager.get_basic_family_id() &&
|
||||
to_app(e)->get_family_id() == m.get_basic_family_id() &&
|
||||
to_app(e)->get_decl_kind() == k &&
|
||||
to_app(e)->get_num_args() == 1) {
|
||||
t = to_app(e)->get_arg(0);
|
||||
|
@ -953,7 +1076,7 @@ bool proof_checker::match_oeq(expr* e, expr_ref& t1, expr_ref& t2) {
|
|||
}
|
||||
|
||||
bool proof_checker::match_negated(expr* a, expr* b) {
|
||||
expr_ref t(m_manager);
|
||||
expr_ref t(m);
|
||||
return
|
||||
(match_not(a, t) && t.get() == b) ||
|
||||
(match_not(b, t) && t.get() == a);
|
||||
|
@ -961,7 +1084,7 @@ bool proof_checker::match_negated(expr* a, expr* b) {
|
|||
|
||||
void proof_checker::get_ors(expr* e, expr_ref_vector& ors) {
|
||||
ptr_buffer<expr> buffer;
|
||||
if (m_manager.is_or(e)) {
|
||||
if (m.is_or(e)) {
|
||||
app* a = to_app(e);
|
||||
ors.append(a->get_num_args(), a->get_args());
|
||||
}
|
||||
|
@ -974,12 +1097,12 @@ void proof_checker::get_ors(expr* e, expr_ref_vector& ors) {
|
|||
void proof_checker::get_hypotheses(proof* p, expr_ref_vector& ante) {
|
||||
ptr_vector<proof> stack;
|
||||
expr* h = 0;
|
||||
expr_ref hyp(m_manager);
|
||||
expr_ref hyp(m);
|
||||
|
||||
stack.push_back(p);
|
||||
while (!stack.empty()) {
|
||||
p = stack.back();
|
||||
SASSERT(m_manager.is_proof(p));
|
||||
SASSERT(m.is_proof(p));
|
||||
if (m_hypotheses.contains(p)) {
|
||||
stack.pop_back();
|
||||
continue;
|
||||
|
@ -992,15 +1115,15 @@ void proof_checker::get_hypotheses(proof* p, expr_ref_vector& ante) {
|
|||
continue;
|
||||
}
|
||||
// in this system all hypotheses get bound by lemmas.
|
||||
if (m_manager.is_lemma(p)) {
|
||||
if (m.is_lemma(p)) {
|
||||
m_hypotheses.insert(p, mk_nil());
|
||||
stack.pop_back();
|
||||
continue;
|
||||
}
|
||||
bool all_found = true;
|
||||
ptr_vector<expr> hyps;
|
||||
for (unsigned i = 0; i < m_manager.get_num_parents(p); ++i) {
|
||||
proof* p_i = m_manager.get_parent(p, i);
|
||||
for (unsigned i = 0; i < m.get_num_parents(p); ++i) {
|
||||
proof* p_i = m.get_parent(p, i);
|
||||
if (m_hypotheses.find(p_i, h)) {
|
||||
hyps.push_back(h);
|
||||
}
|
||||
|
@ -1028,7 +1151,7 @@ void proof_checker::get_hypotheses(proof* p, expr_ref_vector& ante) {
|
|||
ptr_buffer<expr> todo;
|
||||
expr_mark mark;
|
||||
todo.push_back(h);
|
||||
expr_ref a(m_manager), b(m_manager);
|
||||
expr_ref a(m), b(m);
|
||||
|
||||
while (!todo.empty()) {
|
||||
h = todo.back();
|
||||
|
@ -1051,10 +1174,10 @@ void proof_checker::get_hypotheses(proof* p, expr_ref_vector& ante) {
|
|||
}
|
||||
TRACE("proof_checker",
|
||||
{
|
||||
ast_ll_pp(tout << "Getting hypotheses from: ", m_manager, p);
|
||||
ast_ll_pp(tout << "Getting hypotheses from: ", m, p);
|
||||
tout << "Found hypotheses:\n";
|
||||
for (unsigned i = 0; i < ante.size(); ++i) {
|
||||
ast_ll_pp(tout, m_manager, ante[i].get());
|
||||
ast_ll_pp(tout, m, ante[i].get());
|
||||
}
|
||||
});
|
||||
|
||||
|
@ -1090,11 +1213,11 @@ bool proof_checker::match_atom(expr* e, expr_ref& a) const {
|
|||
}
|
||||
|
||||
expr* proof_checker::mk_atom(expr* e) {
|
||||
return m_manager.mk_app(m_hyp_fid, OP_ATOM, e);
|
||||
return m.mk_app(m_hyp_fid, OP_ATOM, e);
|
||||
}
|
||||
|
||||
expr* proof_checker::mk_cons(expr* a, expr* b) {
|
||||
return m_manager.mk_app(m_hyp_fid, OP_CONS, a, b);
|
||||
return m.mk_app(m_hyp_fid, OP_CONS, a, b);
|
||||
}
|
||||
|
||||
expr* proof_checker::mk_nil() {
|
||||
|
@ -1103,7 +1226,7 @@ expr* proof_checker::mk_nil() {
|
|||
|
||||
bool proof_checker::is_hypothesis(proof* p) const {
|
||||
return
|
||||
m_manager.is_proof(p) &&
|
||||
m.is_proof(p) &&
|
||||
p->get_decl_kind() == PR_HYPOTHESIS;
|
||||
}
|
||||
|
||||
|
@ -1130,14 +1253,14 @@ expr* proof_checker::mk_hyp(unsigned num_hyps, expr * const * hyps) {
|
|||
void proof_checker::dump_proof(proof * pr) {
|
||||
if (!m_dump_lemmas)
|
||||
return;
|
||||
SASSERT(m_manager.has_fact(pr));
|
||||
expr * consequent = m_manager.get_fact(pr);
|
||||
unsigned num = m_manager.get_num_parents(pr);
|
||||
SASSERT(m.has_fact(pr));
|
||||
expr * consequent = m.get_fact(pr);
|
||||
unsigned num = m.get_num_parents(pr);
|
||||
ptr_buffer<expr> antecedents;
|
||||
for (unsigned i = 0; i < num; i++) {
|
||||
proof * a = m_manager.get_parent(pr, i);
|
||||
SASSERT(m_manager.has_fact(a));
|
||||
antecedents.push_back(m_manager.get_fact(a));
|
||||
proof * a = m.get_parent(pr, i);
|
||||
SASSERT(m.has_fact(a));
|
||||
antecedents.push_back(m.get_fact(a));
|
||||
}
|
||||
dump_proof(antecedents.size(), antecedents.c_ptr(), consequent);
|
||||
}
|
||||
|
@ -1150,21 +1273,20 @@ void proof_checker::dump_proof(unsigned num_antecedents, expr * const * antecede
|
|||
sprintf(buffer, "proof_lemma_%d.smt", m_proof_lemma_id);
|
||||
#endif
|
||||
std::ofstream out(buffer);
|
||||
ast_smt_pp pp(m_manager);
|
||||
ast_smt_pp pp(m);
|
||||
pp.set_benchmark_name("lemma");
|
||||
pp.set_status("unsat");
|
||||
pp.set_logic(m_logic.c_str());
|
||||
for (unsigned i = 0; i < num_antecedents; i++)
|
||||
pp.add_assumption(antecedents[i]);
|
||||
expr_ref n(m_manager);
|
||||
n = m_manager.mk_not(consequent);
|
||||
expr_ref n(m);
|
||||
n = m.mk_not(consequent);
|
||||
pp.display(out, n);
|
||||
out.close();
|
||||
m_proof_lemma_id++;
|
||||
}
|
||||
|
||||
bool proof_checker::check_arith_literal(bool is_pos, app* lit0, rational const& coeff, expr_ref& sum, bool& is_strict) {
|
||||
ast_manager& m = m_manager;
|
||||
arith_util a(m);
|
||||
app* lit = lit0;
|
||||
|
||||
|
@ -1173,7 +1295,7 @@ bool proof_checker::check_arith_literal(bool is_pos, app* lit0, rational const&
|
|||
is_pos = !is_pos;
|
||||
}
|
||||
if (!a.is_le(lit) && !a.is_lt(lit) && !a.is_ge(lit) && !a.is_gt(lit) && !m.is_eq(lit)) {
|
||||
std::cout << mk_pp(lit, m) << "\n";
|
||||
IF_VERBOSE(0, verbose_stream() << mk_pp(lit, m) << "\n";);
|
||||
return false;
|
||||
}
|
||||
SASSERT(lit->get_num_args() == 2);
|
||||
|
@ -1237,7 +1359,7 @@ bool proof_checker::check_arith_literal(bool is_pos, app* lit0, rational const&
|
|||
rw(sum);
|
||||
}
|
||||
|
||||
std::cout << coeff << "\n" << mk_pp(lit0, m) << "\n" << mk_pp(sum, m) << "\n";
|
||||
IF_VERBOSE(0, verbose_stream() << coeff << "\n" << mk_pp(lit0, m) << "\n" << mk_pp(sum, m) << "\n";);
|
||||
#endif
|
||||
|
||||
return true;
|
||||
|
@ -1247,7 +1369,6 @@ bool proof_checker::check_arith_proof(proof* p) {
|
|||
func_decl* d = p->get_decl();
|
||||
SASSERT(PR_TH_LEMMA == p->get_decl_kind());
|
||||
SASSERT(d->get_parameter(0).get_symbol() == "arith");
|
||||
ast_manager& m = m_manager;
|
||||
unsigned num_params = d->get_num_parameters();
|
||||
arith_util autil(m);
|
||||
|
||||
|
@ -1257,7 +1378,7 @@ bool proof_checker::check_arith_proof(proof* p) {
|
|||
return true;
|
||||
}
|
||||
expr_ref fact(m);
|
||||
proof_ref_vector proofs(m_manager);
|
||||
proof_ref_vector proofs(m);
|
||||
|
||||
if (!match_fact(p, fact)) {
|
||||
UNREACHABLE();
|
||||
|
@ -1331,7 +1452,7 @@ bool proof_checker::check_arith_proof(proof* p) {
|
|||
rw(sum);
|
||||
|
||||
if (!m.is_false(sum)) {
|
||||
std::cout << "Arithmetic proof check failed: " << mk_pp(sum, m) << "\n";
|
||||
IF_VERBOSE(0, verbose_stream() << "Arithmetic proof check failed: " << mk_pp(sum, m) << "\n";);
|
||||
m_dump_lemmas = true;
|
||||
dump_proof(p);
|
||||
return false;
|
||||
|
|
|
@ -23,7 +23,7 @@ Revision History:
|
|||
#include "map.h"
|
||||
|
||||
class proof_checker {
|
||||
ast_manager& m_manager;
|
||||
ast_manager& m;
|
||||
proof_ref_vector m_todo;
|
||||
expr_mark m_marked;
|
||||
expr_ref_vector m_pinned;
|
||||
|
@ -111,6 +111,8 @@ private:
|
|||
expr* mk_hyp(unsigned num_hyps, expr * const * hyps);
|
||||
void dump_proof(proof * pr);
|
||||
void dump_proof(unsigned num_antecedents, expr * const * antecedents, expr * consequent);
|
||||
|
||||
void set_false(expr_ref& e, unsigned idx, expr_ref& lit);
|
||||
};
|
||||
|
||||
#endif
|
||||
|
|
|
@ -459,7 +459,8 @@ bool cmd_context::logic_has_arith_core(symbol const & s) const {
|
|||
s == "UFNIA" ||
|
||||
s == "LIA" ||
|
||||
s == "LRA" ||
|
||||
s == "QF_FPA" ;
|
||||
s == "QF_FPA" ||
|
||||
s == "HORN";
|
||||
}
|
||||
|
||||
bool cmd_context::logic_has_arith() const {
|
||||
|
@ -479,6 +480,12 @@ bool cmd_context::logic_has_bv_core(symbol const & s) const {
|
|||
s == "QF_BVRE";
|
||||
}
|
||||
|
||||
bool cmd_context::logic_has_horn(symbol const& s) const {
|
||||
return
|
||||
s == "HORN";
|
||||
|
||||
}
|
||||
|
||||
bool cmd_context::logic_has_bv() const {
|
||||
return !has_logic() || logic_has_bv_core(m_logic);
|
||||
}
|
||||
|
@ -589,6 +596,7 @@ bool cmd_context::supported_logic(symbol const & s) const {
|
|||
return s == "QF_UF" || s == "UF" ||
|
||||
logic_has_arith_core(s) || logic_has_bv_core(s) ||
|
||||
logic_has_array_core(s) || logic_has_seq_core(s) ||
|
||||
logic_has_horn(s) ||
|
||||
s == "QF_FPA";
|
||||
}
|
||||
|
||||
|
|
|
@ -233,6 +233,7 @@ protected:
|
|||
bool logic_has_bv_core(symbol const & s) const;
|
||||
bool logic_has_array_core(symbol const & s) const;
|
||||
bool logic_has_seq_core(symbol const & s) const;
|
||||
bool logic_has_horn(symbol const& s) const;
|
||||
bool logic_has_arith() const;
|
||||
bool logic_has_bv() const;
|
||||
bool logic_has_seq() const;
|
||||
|
|
|
@ -1096,6 +1096,10 @@ namespace datalog {
|
|||
m_solver.collect_statistics(st);
|
||||
}
|
||||
|
||||
void bmc::reset_statistics() {
|
||||
m_solver.reset_statistics();
|
||||
}
|
||||
|
||||
void bmc::collect_params(param_descrs& p) {
|
||||
}
|
||||
|
||||
|
|
|
@ -127,6 +127,8 @@ namespace datalog {
|
|||
|
||||
void collect_statistics(statistics& st) const;
|
||||
|
||||
void reset_statistics();
|
||||
|
||||
expr_ref get_answer();
|
||||
|
||||
static void collect_params(param_descrs& p);
|
||||
|
|
|
@ -28,20 +28,25 @@ Notes:
|
|||
#include"cancel_eh.h"
|
||||
#include"scoped_ctrl_c.h"
|
||||
#include"scoped_timer.h"
|
||||
#include"trail.h"
|
||||
#include<iomanip>
|
||||
|
||||
|
||||
class dl_context {
|
||||
cmd_context & m_cmd;
|
||||
dl_collected_cmds* m_collected_cmds;
|
||||
unsigned m_ref_count;
|
||||
datalog::dl_decl_plugin* m_decl_plugin;
|
||||
scoped_ptr<datalog::context> m_context;
|
||||
scoped_ptr<datalog::context> m_context;
|
||||
trail_stack<dl_context> m_trail;
|
||||
|
||||
public:
|
||||
dl_context(cmd_context & ctx):
|
||||
dl_context(cmd_context & ctx, dl_collected_cmds* collected_cmds):
|
||||
m_cmd(ctx),
|
||||
m_collected_cmds(collected_cmds),
|
||||
m_ref_count(0),
|
||||
m_decl_plugin(0) {}
|
||||
m_decl_plugin(0),
|
||||
m_trail(*this) {}
|
||||
|
||||
void inc_ref() {
|
||||
++m_ref_count;
|
||||
|
@ -74,14 +79,53 @@ public:
|
|||
void reset() {
|
||||
m_context = 0;
|
||||
}
|
||||
|
||||
void register_predicate(func_decl* pred, unsigned num_kinds, symbol const* kinds) {
|
||||
if (m_collected_cmds) {
|
||||
m_collected_cmds->m_rels.push_back(pred);
|
||||
m_trail.push(push_back_vector<dl_context, func_decl_ref_vector>(m_collected_cmds->m_rels));
|
||||
}
|
||||
dlctx().register_predicate(pred, false);
|
||||
dlctx().set_predicate_representation(pred, num_kinds, kinds);
|
||||
}
|
||||
|
||||
void add_rule(expr * rule, symbol const& name) {
|
||||
init();
|
||||
std::string error_msg;
|
||||
m_context->add_rule(rule, name);
|
||||
if (m_collected_cmds) {
|
||||
expr_ref rl = m_context->bind_variables(rule, true);
|
||||
m_collected_cmds->m_rules.push_back(rl);
|
||||
m_collected_cmds->m_names.push_back(name);
|
||||
m_trail.push(push_back_vector<dl_context, expr_ref_vector>(m_collected_cmds->m_rules));
|
||||
m_trail.push(push_back_vector<dl_context, svector<symbol> >(m_collected_cmds->m_names));
|
||||
}
|
||||
else {
|
||||
m_context->add_rule(rule, name);
|
||||
}
|
||||
}
|
||||
|
||||
bool collect_query(expr* q) {
|
||||
if (m_collected_cmds) {
|
||||
expr_ref qr = m_context->bind_variables(q, false);
|
||||
m_collected_cmds->m_queries.push_back(qr);
|
||||
m_trail.push(push_back_vector<dl_context, expr_ref_vector>(m_collected_cmds->m_queries));
|
||||
return true;
|
||||
}
|
||||
else {
|
||||
return false;
|
||||
}
|
||||
}
|
||||
|
||||
void push() {
|
||||
m_trail.push_scope();
|
||||
dlctx().push();
|
||||
}
|
||||
|
||||
void pop() {
|
||||
m_trail.pop_scope(1);
|
||||
dlctx().pop();
|
||||
}
|
||||
|
||||
datalog::context & get_dl_context() {
|
||||
datalog::context & dlctx() {
|
||||
init();
|
||||
return *m_context;
|
||||
}
|
||||
|
@ -160,7 +204,10 @@ public:
|
|||
if (m_target == 0) {
|
||||
throw cmd_exception("invalid query command, argument expected");
|
||||
}
|
||||
datalog::context& dlctx = m_dl_ctx->get_dl_context();
|
||||
if (m_dl_ctx->collect_query(m_target)) {
|
||||
return;
|
||||
}
|
||||
datalog::context& dlctx = m_dl_ctx->dlctx();
|
||||
set_background(ctx);
|
||||
dlctx.updt_params(m_params);
|
||||
unsigned timeout = m_params.get_uint(":timeout", UINT_MAX);
|
||||
|
@ -217,7 +264,7 @@ public:
|
|||
}
|
||||
|
||||
virtual void init_pdescrs(cmd_context & ctx, param_descrs & p) {
|
||||
m_dl_ctx->get_dl_context().collect_params(p);
|
||||
m_dl_ctx->dlctx().collect_params(p);
|
||||
insert_timeout(p);
|
||||
p.insert(":print-answer", CPK_BOOL, "(default: false) print answer instance(s) to query.");
|
||||
p.insert(":print-certificate", CPK_BOOL, "(default: false) print certificate for reachability or non-reachability.");
|
||||
|
@ -227,7 +274,7 @@ public:
|
|||
|
||||
private:
|
||||
void set_background(cmd_context& ctx) {
|
||||
datalog::context& dlctx = m_dl_ctx->get_dl_context();
|
||||
datalog::context& dlctx = m_dl_ctx->dlctx();
|
||||
ptr_vector<expr>::const_iterator it = ctx.begin_assertions();
|
||||
ptr_vector<expr>::const_iterator end = ctx.end_assertions();
|
||||
for (; it != end; ++it) {
|
||||
|
@ -237,7 +284,7 @@ private:
|
|||
|
||||
void print_answer(cmd_context& ctx) {
|
||||
if (m_params.get_bool(":print-answer", false)) {
|
||||
datalog::context& dlctx = m_dl_ctx->get_dl_context();
|
||||
datalog::context& dlctx = m_dl_ctx->dlctx();
|
||||
ast_manager& m = ctx.m();
|
||||
expr_ref query_result(dlctx.get_answer_as_formula(), m);
|
||||
sbuffer<symbol> var_names;
|
||||
|
@ -253,7 +300,7 @@ private:
|
|||
void print_statistics(cmd_context& ctx) {
|
||||
if (m_params.get_bool(":print-statistics", false)) {
|
||||
statistics st;
|
||||
datalog::context& dlctx = m_dl_ctx->get_dl_context();
|
||||
datalog::context& dlctx = m_dl_ctx->dlctx();
|
||||
unsigned long long max_mem = memory::get_max_used_memory();
|
||||
unsigned long long mem = memory::get_allocation_size();
|
||||
dlctx.collect_statistics(st);
|
||||
|
@ -266,7 +313,7 @@ private:
|
|||
|
||||
void print_certificate(cmd_context& ctx) {
|
||||
if (m_params.get_bool(":print-certificate", false)) {
|
||||
datalog::context& dlctx = m_dl_ctx->get_dl_context();
|
||||
datalog::context& dlctx = m_dl_ctx->dlctx();
|
||||
if (!dlctx.display_certificate(ctx.regular_stream())) {
|
||||
throw cmd_exception("certificates are not supported for selected DL_ENGINE");
|
||||
}
|
||||
|
@ -286,6 +333,7 @@ class dl_declare_rel_cmd : public cmd {
|
|||
void ensure_domain(cmd_context& ctx) {
|
||||
if (!m_domain) m_domain = alloc(sort_ref_vector, ctx.m());
|
||||
}
|
||||
|
||||
public:
|
||||
dl_declare_rel_cmd(dl_context * dl_ctx):
|
||||
cmd("declare-rel"),
|
||||
|
@ -334,11 +382,7 @@ public:
|
|||
func_decl_ref pred(
|
||||
m.mk_func_decl(m_rel_name, m_domain->size(), m_domain->c_ptr(), m.mk_bool_sort()), m);
|
||||
ctx.insert(pred);
|
||||
datalog::context& dctx = m_dl_ctx->get_dl_context();
|
||||
dctx.register_predicate(pred, false);
|
||||
if(!m_kinds.empty()) {
|
||||
dctx.set_predicate_representation(pred, m_kinds.size(), m_kinds.c_ptr());
|
||||
}
|
||||
m_dl_ctx->register_predicate(pred, m_kinds.size(), m_kinds.c_ptr());
|
||||
m_domain = 0;
|
||||
}
|
||||
|
||||
|
@ -385,7 +429,7 @@ public:
|
|||
ast_manager& m = ctx.m();
|
||||
func_decl_ref var(m.mk_func_decl(m_var_name, 0, static_cast<sort*const*>(0), m_var_sort), m);
|
||||
ctx.insert(var);
|
||||
m_dl_ctx->get_dl_context().register_variable(var);
|
||||
m_dl_ctx->dlctx().register_variable(var);
|
||||
}
|
||||
|
||||
};
|
||||
|
@ -402,7 +446,7 @@ public:
|
|||
virtual char const * get_descr(cmd_context & ctx) const { return "push context on the fixedpoint engine"; }
|
||||
|
||||
virtual void execute(cmd_context& ctx) {
|
||||
m_ctx->get_dl_context().push();
|
||||
m_ctx->push();
|
||||
}
|
||||
};
|
||||
|
||||
|
@ -418,19 +462,24 @@ public:
|
|||
virtual char const * get_descr(cmd_context & ctx) const { return "pop context on the fixedpoint engine"; }
|
||||
|
||||
virtual void execute(cmd_context& ctx) {
|
||||
m_ctx->get_dl_context().pop();
|
||||
m_ctx->pop();
|
||||
}
|
||||
};
|
||||
|
||||
|
||||
|
||||
void install_dl_cmds(cmd_context & ctx) {
|
||||
dl_context * dl_ctx = alloc(dl_context, ctx);
|
||||
static void install_dl_cmds_aux(cmd_context& ctx, dl_collected_cmds* collected_cmds) {
|
||||
dl_context * dl_ctx = alloc(dl_context, ctx, collected_cmds);
|
||||
ctx.insert(alloc(dl_rule_cmd, dl_ctx));
|
||||
ctx.insert(alloc(dl_query_cmd, dl_ctx));
|
||||
ctx.insert(alloc(dl_declare_rel_cmd, dl_ctx));
|
||||
ctx.insert(alloc(dl_declare_var_cmd, dl_ctx));
|
||||
PRIVATE_PARAMS(ctx.insert(alloc(dl_push_cmd, dl_ctx));); // not exposed to keep command-extensions simple.
|
||||
PRIVATE_PARAMS(ctx.insert(alloc(dl_pop_cmd, dl_ctx)););
|
||||
PRIVATE_PARAMS(ctx.insert(alloc(dl_pop_cmd, dl_ctx)););
|
||||
}
|
||||
|
||||
void install_dl_cmds(cmd_context & ctx) {
|
||||
install_dl_cmds_aux(ctx, 0);
|
||||
}
|
||||
|
||||
void install_dl_collect_cmds(dl_collected_cmds& collected_cmds, cmd_context & ctx) {
|
||||
install_dl_cmds_aux(ctx, &collected_cmds);
|
||||
}
|
||||
|
|
|
@ -10,7 +10,7 @@ Abstract:
|
|||
|
||||
Author:
|
||||
|
||||
Leonardo (leonardo) 2011-03-28
|
||||
Nikolaj Bjorner (nbjorner) 2012-11-17
|
||||
|
||||
Notes:
|
||||
|
||||
|
@ -18,30 +18,20 @@ Notes:
|
|||
#ifndef _DL_CMDS_H_
|
||||
#define _DL_CMDS_H_
|
||||
|
||||
class cmd;
|
||||
#include "ast.h"
|
||||
|
||||
class cmd_context;
|
||||
|
||||
struct dl_collected_cmds {
|
||||
expr_ref_vector m_rules;
|
||||
svector<symbol> m_names;
|
||||
expr_ref_vector m_queries;
|
||||
func_decl_ref_vector m_rels;
|
||||
dl_collected_cmds(ast_manager& m) : m_rules(m), m_queries(m), m_rels(m) {}
|
||||
};
|
||||
|
||||
void install_dl_cmds(cmd_context & ctx);
|
||||
void install_dl_collect_cmds(dl_collected_cmds& collected_cmds, cmd_context& ctx);
|
||||
|
||||
namespace datalog {
|
||||
|
||||
class context;
|
||||
|
||||
/**
|
||||
Create a command for declaring relations which is connected to
|
||||
a particular datalog context.
|
||||
|
||||
Caller must ensure the returned object is deallocated (e.g. by passing it to a cmd_context).
|
||||
*/
|
||||
cmd * mk_declare_rel_cmd(context& dctx);
|
||||
|
||||
/**
|
||||
Declare a constant as a universal/existential variable.
|
||||
It is implicitly existentially or universally quantified
|
||||
by the rules.
|
||||
*/
|
||||
cmd * mk_declare_var_cmd(context& dctx);
|
||||
|
||||
}
|
||||
|
||||
#endif
|
||||
|
|
|
@ -49,11 +49,14 @@ Revision History:
|
|||
#include"dl_skip_table.h"
|
||||
#endif
|
||||
#include"for_each_expr.h"
|
||||
#include"ast_smt_pp.h"
|
||||
#include"ast_smt2_pp.h"
|
||||
#include"expr_functors.h"
|
||||
#include"dl_mk_partial_equiv.h"
|
||||
#include"dl_mk_bit_blast.h"
|
||||
#include"datatype_decl_plugin.h"
|
||||
#include"expr_abstract.h"
|
||||
|
||||
|
||||
namespace datalog {
|
||||
|
||||
|
@ -331,8 +334,39 @@ namespace datalog {
|
|||
m_vars.push_back(m.mk_const(var));
|
||||
}
|
||||
|
||||
expr_ref context::bind_variables(expr* fml, bool is_forall) {
|
||||
expr_ref result(m);
|
||||
app_ref_vector const& vars = m_vars;
|
||||
if (vars.empty()) {
|
||||
result = fml;
|
||||
}
|
||||
else {
|
||||
ptr_vector<sort> sorts;
|
||||
expr_abstract(m, 0, vars.size(), reinterpret_cast<expr*const*>(vars.c_ptr()), fml, result);
|
||||
get_free_vars(result, sorts);
|
||||
if (sorts.empty()) {
|
||||
result = fml;
|
||||
}
|
||||
else {
|
||||
svector<symbol> names;
|
||||
for (unsigned i = 0; i < sorts.size(); ++i) {
|
||||
if (!sorts[i]) {
|
||||
sorts[i] = m.mk_bool_sort();
|
||||
}
|
||||
names.push_back(symbol(i));
|
||||
}
|
||||
quantifier_ref q(m);
|
||||
q = m.mk_quantifier(is_forall, sorts.size(), sorts.c_ptr(), names.c_ptr(), result);
|
||||
elim_unused_vars(m, q, result);
|
||||
}
|
||||
}
|
||||
return result;
|
||||
}
|
||||
|
||||
void context::register_predicate(func_decl * decl, bool named) {
|
||||
SASSERT(!m_preds.contains(decl));
|
||||
if (m_preds.contains(decl)) {
|
||||
return;
|
||||
}
|
||||
m_pinned.push_back(decl);
|
||||
m_preds.insert(decl);
|
||||
if (named) {
|
||||
|
@ -429,57 +463,35 @@ namespace datalog {
|
|||
}
|
||||
|
||||
void context::set_predicate_representation(func_decl * pred, unsigned relation_name_cnt,
|
||||
symbol * const relation_names) {
|
||||
symbol const * relation_names) {
|
||||
relation_manager & rmgr = get_rmanager();
|
||||
|
||||
family_id target_kind = null_family_id;
|
||||
if (relation_name_cnt==1) {
|
||||
switch (relation_name_cnt) {
|
||||
case 0:
|
||||
return;
|
||||
case 1:
|
||||
target_kind = get_ordinary_relation_plugin(relation_names[0]).get_kind();
|
||||
} else {
|
||||
relation_plugin * tr_plugin = 0; //table plugin, if there is such
|
||||
ptr_vector<relation_plugin> rel_plugins; //plugins that are not table plugins
|
||||
svector<family_id> rel_kinds; //kinds of plugins that are not table plugins
|
||||
for (unsigned i=0; i<relation_name_cnt; i++) {
|
||||
break;
|
||||
default: {
|
||||
svector<family_id> rel_kinds; // kinds of plugins that are not table plugins
|
||||
family_id rel_kind; // the aggregate kind of non-table plugins
|
||||
for (unsigned i = 0; i < relation_name_cnt; i++) {
|
||||
relation_plugin & p = get_ordinary_relation_plugin(relation_names[i]);
|
||||
//commented out, because support combining relations with tables using fpr is not yet implemented
|
||||
/*if (p.from_table()) {
|
||||
if (tr_plugin) {
|
||||
//it does not give any extra benefit to have an intersection of two tables.
|
||||
//Maybe when we can specify which columns belong to which plugin,
|
||||
//it might be of use.
|
||||
throw default_exception("two table plugins cannot be specified as relation type");
|
||||
}
|
||||
tr_plugin = &p;
|
||||
}
|
||||
else {*/
|
||||
rel_plugins.push_back(&p);
|
||||
rel_kinds.push_back(p.get_kind());
|
||||
/*}*/
|
||||
rel_kinds.push_back(p.get_kind());
|
||||
}
|
||||
SASSERT(!rel_kinds.empty());
|
||||
// relation_plugin * rel_plugin; //the aggregate kind of non-table plugins
|
||||
family_id rel_kind; //the aggregate kind of non-table plugins
|
||||
if (rel_kinds.size()==1) {
|
||||
if (rel_kinds.size() == 1) {
|
||||
rel_kind = rel_kinds[0];
|
||||
// rel_plugin = rel_plugins[0];
|
||||
}
|
||||
else {
|
||||
relation_signature rel_sig;
|
||||
//rmgr.from_predicate(pred, rel_sig);
|
||||
product_relation_plugin & prod_plugin = product_relation_plugin::get_plugin(rmgr);
|
||||
rel_kind = prod_plugin.get_relation_kind(rel_sig, rel_kinds);
|
||||
// rel_plugin = &prod_plugin;
|
||||
}
|
||||
if (tr_plugin==0) {
|
||||
target_kind = rel_kind;
|
||||
}
|
||||
else {
|
||||
NOT_IMPLEMENTED_YET();
|
||||
#if 0
|
||||
finite_product_relation_plugin & fprp = finite_product_relation_plugin::get_plugin(rmgr, *rel_plugin);
|
||||
finite_product_relation_plugin::rel_spec spec;
|
||||
#endif
|
||||
}
|
||||
target_kind = rel_kind;
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
||||
SASSERT(target_kind != null_family_id);
|
||||
|
@ -958,7 +970,8 @@ namespace datalog {
|
|||
p.insert(":output-profile", CPK_BOOL, "determines whether profile informations should be output when outputting Datalog rules or instructions");
|
||||
p.insert(":output-tuples", CPK_BOOL, "determines whether tuples for output predicates should be output");
|
||||
p.insert(":profile-timeout-milliseconds", CPK_UINT, "instructions and rules that took less than the threshold will not be printed when printed the instruction/rule list");
|
||||
|
||||
|
||||
p.insert(":print-with-fixedpoint-extensions", CPK_BOOL, "(default true) use SMT-LIB2 fixedpoint extensions, instead of pure SMT2, when printing rules");
|
||||
PRIVATE_PARAMS(
|
||||
p.insert(":dbg-fpr-nonempty-relation-signature", CPK_BOOL,
|
||||
"if true, finite_product_relation will attempt to avoid creating inner relation with empty signature "
|
||||
|
@ -1198,7 +1211,6 @@ namespace datalog {
|
|||
case DATALOG_ENGINE:
|
||||
return dl_query(query);
|
||||
case PDR_ENGINE:
|
||||
return pdr_query(query);
|
||||
case QPDR_ENGINE:
|
||||
return pdr_query(query);
|
||||
case BMC_ENGINE:
|
||||
|
@ -1219,6 +1231,28 @@ namespace datalog {
|
|||
m_last_answer = get_manager().mk_true();
|
||||
}
|
||||
|
||||
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));
|
||||
}
|
||||
}
|
||||
|
||||
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);
|
||||
}
|
||||
}
|
||||
|
||||
void context::ensure_pdr() {
|
||||
if (!m_pdr.get()) {
|
||||
m_pdr = alloc(pdr::dl_interface, *this);
|
||||
|
@ -1479,13 +1513,12 @@ namespace datalog {
|
|||
case DATALOG_ENGINE:
|
||||
return false;
|
||||
case PDR_ENGINE:
|
||||
m_pdr->display_certificate(out);
|
||||
return true;
|
||||
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;
|
||||
default:
|
||||
|
@ -1493,20 +1526,31 @@ namespace datalog {
|
|||
}
|
||||
}
|
||||
|
||||
void context::reset_statistics() {
|
||||
if (m_pdr) {
|
||||
m_pdr->reset_statistics();
|
||||
}
|
||||
if (m_bmc) {
|
||||
m_bmc->reset_statistics();
|
||||
}
|
||||
}
|
||||
|
||||
void context::collect_statistics(statistics& st) {
|
||||
switch(get_engine()) {
|
||||
void context::collect_statistics(statistics& st) const {
|
||||
|
||||
switch(m_engine) {
|
||||
case DATALOG_ENGINE:
|
||||
break;
|
||||
case PDR_ENGINE:
|
||||
m_pdr->collect_statistics(st);
|
||||
break;
|
||||
case QPDR_ENGINE:
|
||||
m_pdr->collect_statistics(st);
|
||||
if (m_pdr) {
|
||||
m_pdr->collect_statistics(st);
|
||||
}
|
||||
break;
|
||||
case BMC_ENGINE:
|
||||
case QBMC_ENGINE:
|
||||
m_bmc->collect_statistics(st);
|
||||
if (m_bmc) {
|
||||
m_bmc->collect_statistics(st);
|
||||
}
|
||||
break;
|
||||
default:
|
||||
break;
|
||||
|
@ -1564,11 +1608,14 @@ namespace datalog {
|
|||
expr* const* axioms = m_background.c_ptr();
|
||||
expr_ref fml(m);
|
||||
expr_ref_vector rules(m);
|
||||
svector<symbol> names;
|
||||
bool use_fixedpoint_extensions = m_params.get_bool(":print-with-fixedpoint-extensions", true);
|
||||
{
|
||||
rule_set::iterator it = m_rule_set.begin(), end = m_rule_set.end();
|
||||
for (; it != end; ++it) {
|
||||
(*it)->to_formula(fml);
|
||||
rules.push_back(fml);
|
||||
names.push_back((*it)->name());
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -1586,13 +1633,17 @@ namespace datalog {
|
|||
if (f->get_family_id() != null_family_id) {
|
||||
//
|
||||
}
|
||||
else if (is_predicate(f)) {
|
||||
else if (is_predicate(f) && use_fixedpoint_extensions) {
|
||||
rels.insert(f);
|
||||
}
|
||||
else {
|
||||
funcs.insert(f);
|
||||
}
|
||||
}
|
||||
|
||||
if (!use_fixedpoint_extensions) {
|
||||
out << "(set-logic HORN)\n";
|
||||
}
|
||||
|
||||
it = funcs.begin(), end = funcs.end();
|
||||
|
||||
|
@ -1619,23 +1670,51 @@ namespace datalog {
|
|||
out << "))\n";
|
||||
}
|
||||
|
||||
declare_vars(rules, fresh_names, out);
|
||||
|
||||
if (use_fixedpoint_extensions) {
|
||||
declare_vars(rules, fresh_names, out);
|
||||
}
|
||||
|
||||
for (unsigned i = 0; i < num_axioms; ++i) {
|
||||
SASSERT(use_fixedpoint_extensions);
|
||||
out << "(assert ";
|
||||
ast_smt2_pp(out, axioms[i], env, params);
|
||||
out << ")\n";
|
||||
}
|
||||
for (unsigned i = 0; i < rules.size(); ++i) {
|
||||
out << "(rule ";
|
||||
ast_smt2_pp(out, rules[i].get(), env, params);
|
||||
for (unsigned i = 0; i < rules.size(); ++i) {
|
||||
out << (use_fixedpoint_extensions?"(rule ":"(assert ");
|
||||
expr* r = rules[i].get();
|
||||
if (symbol::null != names[i]) {
|
||||
out << "(! ";
|
||||
}
|
||||
if (use_fixedpoint_extensions) {
|
||||
ast_smt2_pp(out, r, env, params);
|
||||
}
|
||||
else {
|
||||
out << mk_smt_pp(r, m);
|
||||
}
|
||||
if (symbol::null != names[i]) {
|
||||
out << " :named " << names[i] << ")";
|
||||
}
|
||||
out << ")\n";
|
||||
}
|
||||
for (unsigned i = 0; i < num_queries; ++i) {
|
||||
out << "(query ";
|
||||
ast_smt2_pp(out, queries[i], env, params);
|
||||
out << ")\n";
|
||||
if (use_fixedpoint_extensions) {
|
||||
for (unsigned i = 0; i < num_queries; ++i) {
|
||||
out << "(query ";
|
||||
ast_smt2_pp(out, queries[i], env, params);
|
||||
out << ")\n";
|
||||
}
|
||||
}
|
||||
else {
|
||||
for (unsigned i = 0; i < num_queries; ++i) {
|
||||
if (num_queries > 1) out << "(push)\n";
|
||||
out << "(assert ";
|
||||
expr_ref q(m);
|
||||
q = m.mk_not(queries[i]);
|
||||
ast_smt2_pp(out, q, env, params);
|
||||
out << ")\n";
|
||||
out << "(check-sat)\n";
|
||||
if (num_queries > 1) out << "(pop)\n";
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
@ -184,7 +184,7 @@ namespace datalog {
|
|||
|
||||
void register_variable(func_decl* var);
|
||||
|
||||
app_ref_vector const& get_variables() const { return m_vars; }
|
||||
expr_ref bind_variables(expr* fml, bool is_forall);
|
||||
|
||||
/**
|
||||
Register datalog relation.
|
||||
|
@ -242,7 +242,7 @@ namespace datalog {
|
|||
symbol get_argument_name(const func_decl * pred, unsigned arg_index);
|
||||
|
||||
void set_predicate_representation(func_decl * pred, unsigned relation_name_cnt,
|
||||
symbol * const relation_names);
|
||||
symbol const * relation_names);
|
||||
|
||||
void set_output_predicate(func_decl * pred);
|
||||
bool is_output_predicate(func_decl * pred) { return m_output_preds.contains(pred); }
|
||||
|
@ -383,6 +383,21 @@ namespace datalog {
|
|||
|
||||
lbool query(expr* q);
|
||||
|
||||
/**
|
||||
\brief retrieve model from inductive invariant that shows query is unsat.
|
||||
|
||||
\pre engine == 'pdr' - this option is only supported for PDR mode.
|
||||
*/
|
||||
model_ref get_model();
|
||||
|
||||
/**
|
||||
\brief retrieve proof from derivation of the query.
|
||||
|
||||
\pre engine == 'pdr' - this option is only supported for PDR mode.
|
||||
*/
|
||||
proof_ref get_proof();
|
||||
|
||||
|
||||
/**
|
||||
Query multiple output relations.
|
||||
*/
|
||||
|
@ -411,7 +426,9 @@ namespace datalog {
|
|||
expr* get_answer_as_formula();
|
||||
|
||||
|
||||
void collect_statistics(statistics& st);
|
||||
void collect_statistics(statistics& st) const;
|
||||
|
||||
void reset_statistics();
|
||||
|
||||
/**
|
||||
\brief Display a certificate for reachability and/or unreachability.
|
||||
|
|
|
@ -116,16 +116,20 @@ namespace datalog {
|
|||
apply(src, false, UINT_MAX, tail, tail_neg);
|
||||
mk_rule_inliner::remove_duplicate_tails(tail, tail_neg);
|
||||
SASSERT(tail.size()==tail_neg.size());
|
||||
res = m_rm.mk(new_head, tail.size(), tail.c_ptr(), tail_neg.c_ptr());
|
||||
res = m_rm.mk(new_head, tail.size(), tail.c_ptr(), tail_neg.c_ptr(), tgt.name(), m_normalize);
|
||||
res->set_accounting_parent_object(m_context, const_cast<rule*>(&tgt));
|
||||
res->norm_vars(m_rm);
|
||||
m_rm.fix_unbound_vars(res, true);
|
||||
if (m_interp_simplifier.transform_rule(res.get(), simpl_rule)) {
|
||||
res = simpl_rule;
|
||||
return true;
|
||||
if (m_normalize) {
|
||||
m_rm.fix_unbound_vars(res, true);
|
||||
if (m_interp_simplifier.transform_rule(res.get(), simpl_rule)) {
|
||||
res = simpl_rule;
|
||||
return true;
|
||||
}
|
||||
else {
|
||||
return false;
|
||||
}
|
||||
}
|
||||
else {
|
||||
return false;
|
||||
return true;
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
@ -38,11 +38,12 @@ namespace datalog {
|
|||
substitution m_subst;
|
||||
unifier m_unif;
|
||||
bool m_ready;
|
||||
bool m_normalize;
|
||||
unsigned m_deltas[2];
|
||||
public:
|
||||
rule_unifier(context& ctx)
|
||||
: m(ctx.get_manager()), m_rm(ctx.get_rule_manager()), m_context(ctx),
|
||||
m_interp_simplifier(ctx), m_subst(m), m_unif(m), m_ready(false) {}
|
||||
m_interp_simplifier(ctx), m_subst(m), m_unif(m), m_ready(false), m_normalize(true) {}
|
||||
|
||||
/** Reset subtitution and unify tail tgt_idx of the target rule and the head of the src rule */
|
||||
bool unify_rules(rule const& tgt, unsigned tgt_idx, rule const& src);
|
||||
|
@ -60,6 +61,13 @@ namespace datalog {
|
|||
*/
|
||||
expr_ref_vector get_rule_subst(rule const& r, bool is_tgt);
|
||||
|
||||
/**
|
||||
Control if bound variables are normalized after unification.
|
||||
The default is 'true': bound variables are re-mapped to an
|
||||
initial segment of de-Bruijn indices.
|
||||
*/
|
||||
void set_normalize(bool n) { m_normalize = n; }
|
||||
|
||||
private:
|
||||
void apply(app * a, bool is_tgt, app_ref& res);
|
||||
|
||||
|
|
|
@ -33,7 +33,6 @@ Revision History:
|
|||
#include"for_each_expr.h"
|
||||
#include"used_vars.h"
|
||||
#include"var_subst.h"
|
||||
#include"expr_abstract.h"
|
||||
#include"rewriter_def.h"
|
||||
#include"th_rewriter.h"
|
||||
#include"ast_smt2_pp.h"
|
||||
|
@ -291,30 +290,7 @@ namespace datalog {
|
|||
}
|
||||
|
||||
void rule_manager::bind_variables(expr* fml, bool is_forall, expr_ref& result) {
|
||||
app_ref_vector const& vars = m_ctx.get_variables();
|
||||
if (vars.empty()) {
|
||||
result = fml;
|
||||
}
|
||||
else {
|
||||
ptr_vector<sort> sorts;
|
||||
expr_abstract(m, 0, vars.size(), reinterpret_cast<expr*const*>(vars.c_ptr()), fml, result);
|
||||
get_free_vars(result, sorts);
|
||||
if (sorts.empty()) {
|
||||
result = fml;
|
||||
}
|
||||
else {
|
||||
svector<symbol> names;
|
||||
for (unsigned i = 0; i < sorts.size(); ++i) {
|
||||
if (!sorts[i]) {
|
||||
sorts[i] = m.mk_bool_sort();
|
||||
}
|
||||
names.push_back(symbol(i));
|
||||
}
|
||||
quantifier_ref q(m);
|
||||
q = m.mk_quantifier(is_forall, sorts.size(), sorts.c_ptr(), names.c_ptr(), result);
|
||||
elim_unused_vars(m, q, result);
|
||||
}
|
||||
}
|
||||
result = m_ctx.bind_variables(fml, is_forall);
|
||||
}
|
||||
|
||||
void rule_manager::flatten_body(app_ref_vector& body) {
|
||||
|
@ -526,7 +502,7 @@ namespace datalog {
|
|||
}
|
||||
}
|
||||
|
||||
rule * rule_manager::mk(app * head, unsigned n, app * const * tail, bool const * is_negated, symbol const& name) {
|
||||
rule * rule_manager::mk(app * head, unsigned n, app * const * tail, bool const * is_negated, symbol const& name, bool normalize) {
|
||||
DEBUG_CODE(check_valid_rule(head, n, tail););
|
||||
unsigned sz = rule::get_obj_size(n);
|
||||
void * mem = m.get_allocator().allocate(sz);
|
||||
|
@ -588,7 +564,9 @@ namespace datalog {
|
|||
r->m_positive_cnt = r->m_uninterp_cnt;
|
||||
}
|
||||
|
||||
r->norm_vars(*this);
|
||||
if (normalize) {
|
||||
r->norm_vars(*this);
|
||||
}
|
||||
return r;
|
||||
}
|
||||
|
||||
|
@ -823,7 +801,7 @@ namespace datalog {
|
|||
new_tail.push_back(to_app(tmp));
|
||||
tail_neg.push_back(r->is_neg_tail(i));
|
||||
}
|
||||
r = mk(new_head.get(), new_tail.size(), new_tail.c_ptr(), tail_neg.c_ptr(), r->name());
|
||||
r = mk(new_head.get(), new_tail.size(), new_tail.c_ptr(), tail_neg.c_ptr(), r->name(), false);
|
||||
|
||||
// keep old variable indices around so we can compose with substitutions.
|
||||
// r->norm_vars(*this);
|
||||
|
@ -1068,24 +1046,25 @@ namespace datalog {
|
|||
us(fml);
|
||||
sorts.reverse();
|
||||
|
||||
for (unsigned i = 0; i < sorts.size(); ) {
|
||||
for (unsigned i = 0; i < sorts.size(); ++i) {
|
||||
if (!sorts[i]) {
|
||||
sorts[i] = m.mk_bool_sort();
|
||||
}
|
||||
for (unsigned j = 0; i < sorts.size(); ++j) {
|
||||
for (char c = 'A'; i < sorts.size() && c <= 'Z'; ++c) {
|
||||
func_decl_ref f(m);
|
||||
std::stringstream _name;
|
||||
_name << c;
|
||||
if (j > 0) _name << j;
|
||||
symbol name(_name.str().c_str());
|
||||
if (!us.contains(name)) {
|
||||
names.push_back(name);
|
||||
++i;
|
||||
}
|
||||
}
|
||||
|
||||
for (unsigned j = 0, i = 0; i < sorts.size(); ++j) {
|
||||
for (char c = 'A'; i < sorts.size() && c <= 'Z'; ++c) {
|
||||
func_decl_ref f(m);
|
||||
std::stringstream _name;
|
||||
_name << c;
|
||||
if (j > 0) _name << j;
|
||||
symbol name(_name.str().c_str());
|
||||
if (!us.contains(name)) {
|
||||
names.push_back(name);
|
||||
++i;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
fml = m.mk_forall(sorts.size(), sorts.c_ptr(), names.c_ptr(), fml);
|
||||
}
|
||||
|
||||
|
|
|
@ -116,7 +116,7 @@ namespace datalog {
|
|||
\remark A tail may contain negation. tail[i] is assumed to be negated if is_neg != 0 && is_neg[i] == true
|
||||
*/
|
||||
rule * mk(app * head, unsigned n, app * const * tail, bool const * is_neg = 0,
|
||||
symbol const& name = symbol::null);
|
||||
symbol const& name = symbol::null, bool normalize = true);
|
||||
|
||||
/**
|
||||
\brief Create a rule with the same tail as \c source and with a specified head.
|
||||
|
@ -252,7 +252,7 @@ namespace datalog {
|
|||
|
||||
std::ostream& display_smt2(ast_manager& m, std::ostream & out) const;
|
||||
|
||||
symbol const& name() { return m_name; }
|
||||
symbol const& name() const { return m_name; }
|
||||
|
||||
unsigned hash() const;
|
||||
|
||||
|
|
|
@ -20,9 +20,6 @@ Revision History:
|
|||
|
||||
Notes:
|
||||
|
||||
TODO:
|
||||
- fix the slicing with covers.
|
||||
-
|
||||
|
||||
--*/
|
||||
|
||||
|
@ -101,6 +98,12 @@ namespace pdr {
|
|||
}
|
||||
st.update("PDR num properties", np);
|
||||
}
|
||||
|
||||
void pred_transformer::reset_statistics() {
|
||||
m_solver.reset_statistics();
|
||||
m_reachable.reset_statistics();
|
||||
m_stats.reset();
|
||||
}
|
||||
|
||||
void pred_transformer::init_sig() {
|
||||
if (m_sig.empty()) {
|
||||
|
@ -972,6 +975,7 @@ namespace pdr {
|
|||
proof_ref_vector trail(m);
|
||||
datalog::rule_ref_vector rules_trail(rm);
|
||||
proof* pr = 0;
|
||||
unifier.set_normalize(false);
|
||||
todo.push_back(m_root);
|
||||
while (!todo.empty()) {
|
||||
model_node* n = todo.back();
|
||||
|
@ -1023,6 +1027,7 @@ namespace pdr {
|
|||
binding_is_id = is_var(v) && to_var(v)->get_idx() == i;
|
||||
}
|
||||
if (rls.size() > 1 || !binding_is_id) {
|
||||
expr_ref tmp(m);
|
||||
vector<expr_ref_vector> substs;
|
||||
svector<std::pair<unsigned,unsigned> > positions;
|
||||
substs.push_back(binding); // TODO base substitution.
|
||||
|
@ -1030,9 +1035,10 @@ namespace pdr {
|
|||
datalog::rule& src = *rls[i];
|
||||
bool unified = unifier.unify_rules(*reduced_rule, 0, src);
|
||||
if (!unified) {
|
||||
std::cout << "Could not unify rules: ";
|
||||
reduced_rule->display(dctx, std::cout);
|
||||
src.display(dctx, std::cout);
|
||||
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);
|
||||
TRACE("pdr",
|
||||
|
@ -1041,8 +1047,15 @@ namespace pdr {
|
|||
}
|
||||
tout << "\n";
|
||||
);
|
||||
|
||||
for (unsigned j = 0; j < substs.size(); ++j) {
|
||||
// TODO. apply sub1 to subst.
|
||||
for (unsigned k = 0; k < substs[j].size(); ++k) {
|
||||
var_subst(m, false)(substs[j][k].get(), sub1.size(), sub1.c_ptr(), tmp);
|
||||
substs[j][k] = tmp;
|
||||
}
|
||||
while (substs[j].size() < sub1.size()) {
|
||||
substs[j].push_back(sub1[substs[j].size()].get());
|
||||
}
|
||||
}
|
||||
|
||||
positions.push_back(std::make_pair(i,0));
|
||||
|
@ -1050,9 +1063,11 @@ namespace pdr {
|
|||
VERIFY(unifier.apply(*reduced_rule.get(), 0, src, r3));
|
||||
reduced_rule = r3;
|
||||
}
|
||||
|
||||
expr_ref fml_concl(m);
|
||||
reduced_rule->to_formula(fml_concl);
|
||||
p1 = m.mk_hyper_resolve(pfs.size(), pfs.c_ptr(), fml_concl, positions, substs);
|
||||
|
||||
}
|
||||
cache.insert(n->state(), p1);
|
||||
rules.insert(n->state(), reduced_rule);
|
||||
|
@ -1335,24 +1350,68 @@ namespace pdr {
|
|||
if (!ok) {
|
||||
IF_VERBOSE(0, verbose_stream() << "proof validation failed\n";);
|
||||
}
|
||||
for (unsigned i = 0; i < side_conditions.size(); ++i) {
|
||||
expr* cond = side_conditions[i].get();
|
||||
expr_ref tmp(m);
|
||||
tmp = m.mk_not(cond);
|
||||
IF_VERBOSE(2, verbose_stream() << "checking side-condition:\n" << mk_pp(cond, m) << "\n";);
|
||||
smt::kernel solver(m, get_fparams());
|
||||
solver.assert_expr(tmp);
|
||||
lbool res = solver.check();
|
||||
if (res != l_false) {
|
||||
IF_VERBOSE(0, verbose_stream() << "rule validation failed\n";
|
||||
verbose_stream() << mk_pp(cond, m) << "\n";
|
||||
);
|
||||
}
|
||||
}
|
||||
break;
|
||||
}
|
||||
case l_false: {
|
||||
expr_ref_vector refs(m);
|
||||
expr_ref_vector refs(m), fmls(m);
|
||||
expr_ref tmp(m);
|
||||
model_ref model;
|
||||
vector<relation_info> rs;
|
||||
model_converter_ref mc;
|
||||
get_level_property(m_inductive_lvl, refs, rs);
|
||||
inductive_property ex(m, const_cast<model_converter_ref&>(m_mc), rs);
|
||||
inductive_property ex(m, mc, rs);
|
||||
ex.to_model(model);
|
||||
decl2rel::iterator it = m_rels.begin(), end = m_rels.end();
|
||||
var_subst vs(m, false);
|
||||
var_subst vs(m, false);
|
||||
for (; it != end; ++it) {
|
||||
ptr_vector<datalog::rule> const& rules = it->m_value->rules();
|
||||
for (unsigned i = 0; i < rules.size(); ++i) {
|
||||
// datalog::rule* rule = rules[i];
|
||||
// vs(rule->get_head(),
|
||||
// apply interpretation of predicates to rule.
|
||||
// create formula and check for unsat.
|
||||
datalog::rule& r = *rules[i];
|
||||
model->eval(r.get_head(), tmp);
|
||||
fmls.push_back(m.mk_not(tmp));
|
||||
unsigned utsz = r.get_uninterpreted_tail_size();
|
||||
unsigned tsz = r.get_tail_size();
|
||||
for (unsigned j = 0; j < utsz; ++j) {
|
||||
model->eval(r.get_tail(j), tmp);
|
||||
fmls.push_back(tmp);
|
||||
}
|
||||
for (unsigned j = utsz; j < tsz; ++j) {
|
||||
fmls.push_back(r.get_tail(j));
|
||||
}
|
||||
tmp = m.mk_and(fmls.size(), fmls.c_ptr());
|
||||
ptr_vector<sort> sorts;
|
||||
svector<symbol> names;
|
||||
get_free_vars(tmp, sorts);
|
||||
for (unsigned i = 0; i < sorts.size(); ++i) {
|
||||
if (!sorts[i]) {
|
||||
sorts[i] = m.mk_bool_sort();
|
||||
}
|
||||
names.push_back(symbol(i));
|
||||
}
|
||||
sorts.reverse();
|
||||
tmp = m.mk_exists(sorts.size(), sorts.c_ptr(), names.c_ptr(), tmp);
|
||||
smt::kernel solver(m, get_fparams());
|
||||
solver.assert_expr(tmp);
|
||||
lbool res = solver.check();
|
||||
if (res != l_false) {
|
||||
IF_VERBOSE(0, verbose_stream() << "rule validation failed\n";
|
||||
verbose_stream() << mk_pp(tmp, m) << "\n";
|
||||
);
|
||||
}
|
||||
}
|
||||
}
|
||||
break;
|
||||
|
@ -1442,7 +1501,14 @@ namespace pdr {
|
|||
simplify_formulas();
|
||||
m_last_result = l_false;
|
||||
TRACE("pdr", display_certificate(tout););
|
||||
IF_VERBOSE(1, display_certificate(verbose_stream()););
|
||||
IF_VERBOSE(1, {
|
||||
expr_ref_vector refs(m);
|
||||
vector<relation_info> rs;
|
||||
get_level_property(m_inductive_lvl, refs, rs);
|
||||
model_converter_ref mc;
|
||||
inductive_property ex(m, mc, rs);
|
||||
verbose_stream() << ex.to_string();
|
||||
});
|
||||
validate();
|
||||
return l_false;
|
||||
}
|
||||
|
@ -1477,13 +1543,15 @@ namespace pdr {
|
|||
}
|
||||
}
|
||||
|
||||
void context::get_model(model_ref& md) {
|
||||
model_ref context::get_model() {
|
||||
SASSERT(m_last_result == l_false);
|
||||
expr_ref_vector refs(m);
|
||||
vector<relation_info> rs;
|
||||
model_ref md;
|
||||
get_level_property(m_inductive_lvl, refs, rs);
|
||||
inductive_property ex(m, m_mc, rs);
|
||||
ex.to_model(md);
|
||||
return md;
|
||||
}
|
||||
|
||||
proof_ref context::get_proof() const {
|
||||
|
@ -1871,6 +1939,20 @@ namespace pdr {
|
|||
}
|
||||
}
|
||||
|
||||
void context::reset_statistics() {
|
||||
decl2rel::iterator it = m_rels.begin(), end = m_rels.end();
|
||||
for (it = m_rels.begin(); it != end; ++it) {
|
||||
it->m_value->reset_statistics();
|
||||
}
|
||||
m_stats.reset();
|
||||
m_pm.reset_statistics();
|
||||
|
||||
for (unsigned i = 0; i < m_core_generalizers.size(); ++i) {
|
||||
m_core_generalizers[i]->reset_statistics();
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
|
||||
std::ostream& context::display(std::ostream& out) const {
|
||||
decl2rel::iterator it = m_rels.begin(), end = m_rels.end();
|
||||
|
|
|
@ -132,6 +132,7 @@ namespace pdr {
|
|||
std::ostream& display(std::ostream& strm) const;
|
||||
|
||||
void collect_statistics(statistics& st) const;
|
||||
void reset_statistics();
|
||||
|
||||
bool is_reachable(expr* state);
|
||||
void remove_predecessors(expr_ref_vector& literals);
|
||||
|
@ -275,6 +276,7 @@ namespace pdr {
|
|||
}
|
||||
}
|
||||
virtual void collect_statistics(statistics& st) const {}
|
||||
virtual void reset_statistics() {}
|
||||
};
|
||||
|
||||
class context {
|
||||
|
@ -366,6 +368,7 @@ namespace pdr {
|
|||
|
||||
|
||||
void collect_statistics(statistics& st) const;
|
||||
void reset_statistics();
|
||||
|
||||
std::ostream& display(std::ostream& strm) const;
|
||||
|
||||
|
@ -401,7 +404,7 @@ namespace pdr {
|
|||
|
||||
void add_cover(int level, func_decl* pred, expr* property);
|
||||
|
||||
void get_model(model_ref& md);
|
||||
model_ref get_model();
|
||||
|
||||
proof_ref get_proof() const;
|
||||
|
||||
|
|
|
@ -197,6 +197,10 @@ void dl_interface::collect_statistics(statistics& st) const {
|
|||
m_context->collect_statistics(st);
|
||||
}
|
||||
|
||||
void dl_interface::reset_statistics() {
|
||||
m_context->reset_statistics();
|
||||
}
|
||||
|
||||
void dl_interface::display_certificate(std::ostream& out) const {
|
||||
m_context->display_certificate(out);
|
||||
}
|
||||
|
@ -218,6 +222,14 @@ void dl_interface::updt_params() {
|
|||
m_context = alloc(pdr::context, m_ctx.get_fparams(), m_ctx.get_params(), m_ctx.get_manager());
|
||||
}
|
||||
|
||||
model_ref dl_interface::get_model() {
|
||||
return m_context->get_model();
|
||||
}
|
||||
|
||||
proof_ref dl_interface::get_proof() {
|
||||
return m_context->get_proof();
|
||||
}
|
||||
|
||||
void dl_interface::collect_params(param_descrs& p) {
|
||||
p.insert(":bfs-model-search", CPK_BOOL, "PDR: (default true) use BFS strategy for expanding model search");
|
||||
p.insert(":use-farkas", CPK_BOOL, "PDR: (default true) use lemma generator based on Farkas (for linear real arithmetic)");
|
||||
|
@ -239,8 +251,8 @@ void dl_interface::collect_params(param_descrs& p) {
|
|||
"checking for reachability (not only during cube weakening)"););
|
||||
PRIVATE_PARAMS(p.insert(":max-num-contexts", CPK_UINT, "PDR: (default 500) maximal number of contexts to create"););
|
||||
PRIVATE_PARAMS(p.insert(":try-minimize-core", CPK_BOOL, "PDR: (default false) try to reduce core size (before inductive minimization)"););
|
||||
PRIVATE_PARAMS(p.insert(":simplify-formulas-pre", CPK_BOOL, "PDR: (default false) simplify derived formulas before inductive propagation"););
|
||||
PRIVATE_PARAMS(p.insert(":simplify-formulas-post", CPK_BOOL, "PDR: (default false) simplify derived formulas after inductive propagation"););
|
||||
p.insert(":simplify-formulas-pre", CPK_BOOL, "PDR: (default false) simplify derived formulas before inductive propagation");
|
||||
p.insert(":simplify-formulas-post", CPK_BOOL, "PDR: (default false) simplify derived formulas after inductive propagation");
|
||||
p.insert(":slice", CPK_BOOL, "PDR: (default true) simplify clause set using slicing");
|
||||
p.insert(":coalesce-rules", CPK_BOOL, "BMC: (default false) coalesce rules");
|
||||
}
|
||||
|
|
|
@ -57,6 +57,8 @@ namespace pdr {
|
|||
|
||||
void collect_statistics(statistics& st) const;
|
||||
|
||||
void reset_statistics();
|
||||
|
||||
expr_ref get_answer();
|
||||
|
||||
unsigned get_num_levels(func_decl* pred);
|
||||
|
@ -66,8 +68,12 @@ namespace pdr {
|
|||
void add_cover(int level, func_decl* pred, expr* property);
|
||||
|
||||
static void collect_params(param_descrs& p);
|
||||
|
||||
|
||||
void updt_params();
|
||||
|
||||
model_ref get_model();
|
||||
|
||||
proof_ref get_proof();
|
||||
|
||||
};
|
||||
}
|
||||
|
|
|
@ -313,6 +313,8 @@ namespace pdr {
|
|||
pdr::smt_context* mk_fresh() { return m_contexts.mk_fresh(); }
|
||||
|
||||
void collect_statistics(statistics& st) const { m_contexts.collect_statistics(st); }
|
||||
|
||||
void reset_statistics() { m_contexts.reset_statistics(); }
|
||||
};
|
||||
}
|
||||
|
||||
|
|
|
@ -364,8 +364,7 @@ namespace pdr {
|
|||
m_core->append(lemmas);
|
||||
}
|
||||
|
||||
lbool prop_solver::check_assumptions(const expr_ref_vector & atoms)
|
||||
{
|
||||
lbool prop_solver::check_assumptions(const expr_ref_vector & atoms) {
|
||||
return check_assumptions_and_formula(atoms, m.mk_true());
|
||||
}
|
||||
|
||||
|
@ -393,5 +392,10 @@ namespace pdr {
|
|||
void prop_solver::collect_statistics(statistics& st) const {
|
||||
}
|
||||
|
||||
void prop_solver::reset_statistics() {
|
||||
}
|
||||
|
||||
|
||||
|
||||
|
||||
}
|
||||
|
|
|
@ -122,6 +122,8 @@ namespace pdr {
|
|||
expr * form);
|
||||
|
||||
void collect_statistics(statistics& st) const;
|
||||
|
||||
void reset_statistics();
|
||||
|
||||
};
|
||||
}
|
||||
|
|
|
@ -27,9 +27,6 @@ namespace pdr {
|
|||
m_ctx(0),
|
||||
m_ref_holder(m),
|
||||
m_disj_connector(m),
|
||||
m_cache_hits(0),
|
||||
m_cache_miss(0),
|
||||
m_cache_inserts(0),
|
||||
m_cache_mode((datalog::PDR_CACHE_MODE)params.get_uint(":cache-mode",0)) {
|
||||
if (m_cache_mode == datalog::CONSTRAINT_CACHE) {
|
||||
m_ctx = pm.mk_fresh();
|
||||
|
@ -63,13 +60,13 @@ namespace pdr {
|
|||
break;
|
||||
|
||||
case datalog::HASH_CACHE:
|
||||
m_cache_inserts++;
|
||||
m_stats.m_inserts++;
|
||||
m_cache.insert(cube);
|
||||
m_ref_holder.push_back(cube);
|
||||
break;
|
||||
|
||||
case datalog::CONSTRAINT_CACHE:
|
||||
m_cache_inserts++;
|
||||
m_stats.m_inserts++;
|
||||
TRACE("pdr", tout << mk_pp(cube, m) << "\n";);
|
||||
add_disjuncted_formula(cube);
|
||||
break;
|
||||
|
@ -112,14 +109,18 @@ namespace pdr {
|
|||
UNREACHABLE();
|
||||
break;
|
||||
}
|
||||
if (found) m_cache_hits++; m_cache_miss++;
|
||||
if (found) m_stats.m_hits++; m_stats.m_miss++;
|
||||
return found;
|
||||
}
|
||||
|
||||
void reachable_cache::collect_statistics(statistics& st) const {
|
||||
st.update("cache inserts", m_cache_inserts);
|
||||
st.update("cache miss", m_cache_miss);
|
||||
st.update("cache hits", m_cache_hits);
|
||||
st.update("cache inserts", m_stats.m_inserts);
|
||||
st.update("cache miss", m_stats.m_miss);
|
||||
st.update("cache hits", m_stats.m_hits);
|
||||
}
|
||||
|
||||
void reachable_cache::reset_statistics() {
|
||||
m_stats.reset();
|
||||
}
|
||||
|
||||
|
||||
|
|
|
@ -28,15 +28,21 @@ Revision History:
|
|||
|
||||
namespace pdr {
|
||||
class reachable_cache {
|
||||
struct stats {
|
||||
unsigned m_hits;
|
||||
unsigned m_miss;
|
||||
unsigned m_inserts;
|
||||
stats() { reset(); }
|
||||
void reset() { memset(this, 0, sizeof(*this)); }
|
||||
};
|
||||
|
||||
ast_manager & m;
|
||||
manager & m_pm;
|
||||
scoped_ptr<smt_context> m_ctx;
|
||||
ast_ref_vector m_ref_holder;
|
||||
app_ref m_disj_connector;
|
||||
obj_hashtable<expr> m_cache;
|
||||
unsigned m_cache_hits;
|
||||
unsigned m_cache_miss;
|
||||
unsigned m_cache_inserts;
|
||||
stats m_stats;
|
||||
datalog::PDR_CACHE_MODE m_cache_mode;
|
||||
|
||||
void add_disjuncted_formula(expr * f);
|
||||
|
@ -53,6 +59,8 @@ namespace pdr {
|
|||
bool is_reachable(expr * cube);
|
||||
|
||||
void collect_statistics(statistics& st) const;
|
||||
|
||||
void reset_statistics();
|
||||
};
|
||||
}
|
||||
|
||||
|
|
|
@ -136,6 +136,12 @@ namespace pdr {
|
|||
}
|
||||
}
|
||||
|
||||
void smt_context_manager::reset_statistics() {
|
||||
for (unsigned i = 0; i < m_contexts.size(); ++i) {
|
||||
m_contexts[i]->reset_statistics();
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
};
|
||||
|
||||
|
|
|
@ -100,6 +100,7 @@ namespace pdr {
|
|||
~smt_context_manager();
|
||||
smt_context* mk_fresh();
|
||||
void collect_statistics(statistics& st) const;
|
||||
void reset_statistics();
|
||||
bool is_aux_predicate(func_decl* p) const { return m_predicate_set.contains(p); }
|
||||
};
|
||||
|
||||
|
|
286
src/muz_qe/pdr_tactic.cpp
Normal file
286
src/muz_qe/pdr_tactic.cpp
Normal file
|
@ -0,0 +1,286 @@
|
|||
/*++
|
||||
Copyright (c) 2012 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
pdr_tactic.h
|
||||
|
||||
Abstract:
|
||||
|
||||
PDR as a tactic to solve Horn clauses.
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2012-11-16.
|
||||
|
||||
Revision History:
|
||||
|
||||
--*/
|
||||
#include"tactical.h"
|
||||
#include"model_converter.h"
|
||||
#include"proof_converter.h"
|
||||
#include"pdr_tactic.h"
|
||||
#include"dl_context.h"
|
||||
|
||||
class pdr_tactic : public tactic {
|
||||
struct imp {
|
||||
ast_manager& m;
|
||||
datalog::context m_ctx;
|
||||
front_end_params m_fparams;
|
||||
|
||||
imp(ast_manager & m, params_ref const & p):
|
||||
m(m),
|
||||
m_ctx(m, m_fparams) {
|
||||
updt_params(p);
|
||||
}
|
||||
|
||||
void updt_params(params_ref const & p) {
|
||||
m_ctx.updt_params(p);
|
||||
}
|
||||
|
||||
void collect_param_descrs(param_descrs & r) {
|
||||
m_ctx.collect_params(r);
|
||||
}
|
||||
|
||||
void reset_statistics() {
|
||||
m_ctx.reset_statistics();
|
||||
}
|
||||
|
||||
void collect_statistics(statistics & st) const {
|
||||
m_ctx.collect_statistics(st);
|
||||
}
|
||||
|
||||
void set_cancel(bool f) {
|
||||
if (f) {
|
||||
m_ctx.cancel();
|
||||
}
|
||||
}
|
||||
|
||||
void normalize(expr_ref& f) {
|
||||
bool is_positive = true;
|
||||
expr* e = 0;
|
||||
while (true) {
|
||||
if (is_forall(f) && is_positive) {
|
||||
f = to_quantifier(f)->get_expr();
|
||||
}
|
||||
else if (is_exists(f) && !is_positive) {
|
||||
f = to_quantifier(f)->get_expr();
|
||||
}
|
||||
else if (m.is_not(f, e)) {
|
||||
is_positive = !is_positive;
|
||||
f = e;
|
||||
}
|
||||
else {
|
||||
break;
|
||||
}
|
||||
}
|
||||
if (!is_positive) {
|
||||
f = m.mk_not(f);
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
bool is_predicate(expr* a) {
|
||||
SASSERT(m.is_bool(a));
|
||||
return is_app(a) && to_app(a)->get_decl()->get_family_id() == null_family_id;
|
||||
}
|
||||
|
||||
void register_predicate(expr* a) {
|
||||
SASSERT(is_predicate(a));
|
||||
m_ctx.register_predicate(to_app(a)->get_decl(), true);
|
||||
}
|
||||
|
||||
enum formula_kind { IS_RULE, IS_QUERY, IS_NONE };
|
||||
|
||||
formula_kind get_formula_kind(expr_ref& f) {
|
||||
normalize(f);
|
||||
expr_ref_vector args(m), body(m);
|
||||
expr_ref head(m);
|
||||
expr* a = 0, *a1 = 0;
|
||||
datalog::flatten_or(f, args);
|
||||
for (unsigned i = 0; i < args.size(); ++i) {
|
||||
a = args[i].get();
|
||||
if (m.is_not(a, a1) && is_predicate(a1)) {
|
||||
register_predicate(a1);
|
||||
body.push_back(a1);
|
||||
}
|
||||
else if (is_predicate(a)) {
|
||||
register_predicate(a);
|
||||
if (head) {
|
||||
return IS_NONE;
|
||||
}
|
||||
head = a;
|
||||
}
|
||||
else if (m.is_not(a, a1)) {
|
||||
body.push_back(a1);
|
||||
}
|
||||
else {
|
||||
body.push_back(m.mk_not(a));
|
||||
}
|
||||
}
|
||||
f = m.mk_and(body.size(), body.c_ptr());
|
||||
if (head) {
|
||||
f = m.mk_implies(f, head);
|
||||
return IS_RULE;
|
||||
}
|
||||
else {
|
||||
return IS_QUERY;
|
||||
}
|
||||
}
|
||||
|
||||
expr_ref mk_rule(expr* body, expr* head) {
|
||||
return expr_ref(m.mk_implies(body, head), m);
|
||||
}
|
||||
|
||||
void operator()(goal_ref const & g,
|
||||
goal_ref_buffer & result,
|
||||
model_converter_ref & mc,
|
||||
proof_converter_ref & pc,
|
||||
expr_dependency_ref & core) {
|
||||
SASSERT(g->is_well_sorted());
|
||||
mc = 0; pc = 0; core = 0;
|
||||
tactic_report report("pdr", *g);
|
||||
bool produce_models = g->models_enabled();
|
||||
bool produce_proofs = g->proofs_enabled();
|
||||
|
||||
if (produce_proofs) {
|
||||
if (!m_ctx.get_params().get_bool(":generate-proof-trace", true)) {
|
||||
params_ref params = m_ctx.get_params();
|
||||
params.set_bool(":generate-proof-trace", true);
|
||||
updt_params(params);
|
||||
}
|
||||
}
|
||||
|
||||
unsigned sz = g->size();
|
||||
expr_ref q(m), f(m);
|
||||
expr_ref_vector queries(m);
|
||||
std::stringstream msg;
|
||||
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
f = g->form(i);
|
||||
formula_kind k = get_formula_kind(f);
|
||||
switch(k) {
|
||||
case IS_RULE:
|
||||
m_ctx.add_rule(f, symbol::null);
|
||||
break;
|
||||
case IS_QUERY:
|
||||
queries.push_back(f);
|
||||
break;
|
||||
default:
|
||||
msg << "formula is not in Horn fragment: " << mk_pp(g->form(i), m) << "\n";
|
||||
throw tactic_exception(msg.str().c_str());
|
||||
}
|
||||
}
|
||||
|
||||
if (queries.size() != 1) {
|
||||
q = m.mk_fresh_const("query", m.mk_bool_sort());
|
||||
for (unsigned i = 0; i < queries.size(); ++i) {
|
||||
f = mk_rule(queries[i].get(), q);
|
||||
m_ctx.add_rule(f, symbol::null);
|
||||
}
|
||||
queries.reset();
|
||||
queries.push_back(q);
|
||||
}
|
||||
SASSERT(queries.size() == 1);
|
||||
q = queries[0].get();
|
||||
lbool is_reachable = m_ctx.query(q);
|
||||
g->inc_depth();
|
||||
result.push_back(g.get());
|
||||
switch (is_reachable) {
|
||||
case l_true: {
|
||||
// goal is unsat
|
||||
g->assert_expr(m.mk_false());
|
||||
if (produce_proofs) {
|
||||
proof_ref proof = m_ctx.get_proof();
|
||||
pc = proof2proof_converter(m, proof);
|
||||
}
|
||||
break;
|
||||
}
|
||||
case l_false: {
|
||||
// goal is sat
|
||||
g->reset();
|
||||
if (produce_models) {
|
||||
model_ref md = m_ctx.get_model();
|
||||
mc = model2model_converter(&*md);
|
||||
}
|
||||
break;
|
||||
}
|
||||
case l_undef:
|
||||
// subgoal is unchanged.
|
||||
break;
|
||||
}
|
||||
TRACE("pdr", g->display(tout););
|
||||
SASSERT(g->is_well_sorted());
|
||||
}
|
||||
};
|
||||
|
||||
params_ref m_params;
|
||||
imp * m_imp;
|
||||
public:
|
||||
pdr_tactic(ast_manager & m, params_ref const & p):
|
||||
m_params(p) {
|
||||
m_imp = alloc(imp, m, p);
|
||||
}
|
||||
|
||||
virtual tactic * translate(ast_manager & m) {
|
||||
return alloc(pdr_tactic, m, m_params);
|
||||
}
|
||||
|
||||
virtual ~pdr_tactic() {
|
||||
dealloc(m_imp);
|
||||
}
|
||||
|
||||
virtual void updt_params(params_ref const & p) {
|
||||
m_params = p;
|
||||
m_imp->updt_params(p);
|
||||
}
|
||||
|
||||
|
||||
virtual void collect_param_descrs(param_descrs & r) {
|
||||
m_imp->collect_param_descrs(r);
|
||||
}
|
||||
|
||||
virtual void operator()(goal_ref const & in,
|
||||
goal_ref_buffer & result,
|
||||
model_converter_ref & mc,
|
||||
proof_converter_ref & pc,
|
||||
expr_dependency_ref & core) {
|
||||
(*m_imp)(in, result, mc, pc, core);
|
||||
}
|
||||
|
||||
|
||||
virtual void collect_statistics(statistics & st) const {
|
||||
m_imp->collect_statistics(st);
|
||||
}
|
||||
|
||||
virtual void reset_statistics() {
|
||||
m_imp->reset_statistics();
|
||||
}
|
||||
|
||||
|
||||
virtual void cleanup() {
|
||||
ast_manager & m = m_imp->m;
|
||||
imp * d = m_imp;
|
||||
#pragma omp critical (tactic_cancel)
|
||||
{
|
||||
m_imp = 0;
|
||||
}
|
||||
dealloc(d);
|
||||
d = alloc(imp, m, m_params);
|
||||
#pragma omp critical (tactic_cancel)
|
||||
{
|
||||
m_imp = d;
|
||||
}
|
||||
}
|
||||
|
||||
protected:
|
||||
virtual void set_cancel(bool f) {
|
||||
if (m_imp)
|
||||
m_imp->set_cancel(f);
|
||||
}
|
||||
};
|
||||
|
||||
tactic * mk_pdr_tactic(ast_manager & m, params_ref const & p) {
|
||||
return clean(alloc(pdr_tactic, m, p));
|
||||
}
|
||||
|
30
src/muz_qe/pdr_tactic.h
Normal file
30
src/muz_qe/pdr_tactic.h
Normal file
|
@ -0,0 +1,30 @@
|
|||
/*++
|
||||
Copyright (c) 2012 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
pdr_tactic.h
|
||||
|
||||
Abstract:
|
||||
|
||||
PDR as a tactic to solve Horn clauses.
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2012-11-16.
|
||||
|
||||
Revision History:
|
||||
|
||||
--*/
|
||||
#ifndef _PDR_TACTIC_H_
|
||||
#define _PDR_TACTIC_H_
|
||||
|
||||
#include"params.h"
|
||||
class ast_manager;
|
||||
class tactic;
|
||||
|
||||
tactic * mk_pdr_tactic(ast_manager & m, params_ref const & p = params_ref());
|
||||
/*
|
||||
ADD_TACTIC("pdr", "apply pdr for horn clauses.", "mk_pdr_tactic(m, p)")
|
||||
*/
|
||||
#endif
|
|
@ -324,13 +324,12 @@ expr_ref_vector model_evaluator::prune_by_cone_of_influence(ptr_vector<expr> con
|
|||
unsigned sz = m_model->get_num_constants();
|
||||
expr_ref e(m), eq(m);
|
||||
expr_ref_vector model(m);
|
||||
bool_rewriter rw(m);
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
func_decl * d = m_model->get_constant(i);
|
||||
expr* val = m_model->get_const_interp(d);
|
||||
e = m.mk_const(d);
|
||||
if (m_visited.is_marked(e)) {
|
||||
rw.mk_eq(e, val, eq);
|
||||
eq = m.mk_eq(e, val);
|
||||
model.push_back(eq);
|
||||
}
|
||||
}
|
||||
|
@ -466,6 +465,7 @@ void model_evaluator::eval_arith(app* e) {
|
|||
}
|
||||
|
||||
void model_evaluator::inherit_value(expr* e, expr* v) {
|
||||
expr* w;
|
||||
SASSERT(!is_unknown(v));
|
||||
SASSERT(m.get_sort(e) == m.get_sort(v));
|
||||
if (is_x(v)) {
|
||||
|
@ -475,7 +475,10 @@ void model_evaluator::inherit_value(expr* e, expr* v) {
|
|||
SASSERT(m.is_bool(v));
|
||||
if (is_true(v)) set_true(e);
|
||||
else if (is_false(v)) set_false(e);
|
||||
else set_x(e);
|
||||
else {
|
||||
TRACE("pdr", tout << "not inherited:\n" << mk_pp(e, m) << "\n" << mk_pp(v, m) << "\n";);
|
||||
set_x(e);
|
||||
}
|
||||
}
|
||||
else if (m_arith.is_int_real(e)) {
|
||||
set_number(e, get_number(v));
|
||||
|
@ -483,7 +486,11 @@ void model_evaluator::inherit_value(expr* e, expr* v) {
|
|||
else if (m.is_value(v)) {
|
||||
set_value(e, v);
|
||||
}
|
||||
else if (m_values.find(v, w)) {
|
||||
set_value(e, w);
|
||||
}
|
||||
else {
|
||||
TRACE("pdr", tout << "not inherited:\n" << mk_pp(e, m) << "\n" << mk_pp(v, m) << "\n";);
|
||||
set_x(e);
|
||||
}
|
||||
}
|
||||
|
@ -642,6 +649,7 @@ void model_evaluator::eval_basic(app* e) {
|
|||
set_bool(e, e1 == e2);
|
||||
}
|
||||
else {
|
||||
TRACE("pdr", tout << "not value equal:\n" << mk_pp(e1, m) << "\n" << mk_pp(e2, m) << "\n";);
|
||||
set_x(e);
|
||||
}
|
||||
}
|
||||
|
|
|
@ -223,7 +223,7 @@ public:
|
|||
found_false = true;
|
||||
break;
|
||||
}
|
||||
SASSERT(m.get_fact(tmp) == m.get_fact(m.get_parent(p, i)));
|
||||
// SASSERT(m.get_fact(tmp) == m.get_fact(m.get_parent(p, i)));
|
||||
parents.push_back(tmp);
|
||||
if (is_closed(tmp) && !m_units.contains(m.get_fact(tmp))) {
|
||||
m_units.insert(m.get_fact(tmp), tmp);
|
||||
|
@ -283,7 +283,7 @@ public:
|
|||
found_false = true;
|
||||
break;
|
||||
}
|
||||
SASSERT(m.get_fact(tmp) == m.get_fact(m.get_parent(p, i)));
|
||||
// SASSERT(m.get_fact(tmp) == m.get_fact(m.get_parent(p, i)));
|
||||
change = change || (tmp != m.get_parent(p, i));
|
||||
args.push_back(tmp);
|
||||
}
|
||||
|
|
|
@ -33,6 +33,7 @@ Notes:
|
|||
#include"default_tactic.h"
|
||||
#include"ufbv_tactic.h"
|
||||
#include"qffpa_tactic.h"
|
||||
#include"pdr_tactic.h"
|
||||
#include"smt_solver.h"
|
||||
|
||||
MK_SIMPLE_TACTIC_FACTORY(qfuf_fct, mk_qfuf_tactic(m, p));
|
||||
|
@ -54,6 +55,7 @@ MK_SIMPLE_TACTIC_FACTORY(qfnia_fct, mk_qfnia_tactic(m, p));
|
|||
MK_SIMPLE_TACTIC_FACTORY(qfnra_fct, mk_qfnra_tactic(m, p));
|
||||
MK_SIMPLE_TACTIC_FACTORY(qffpa_fct, mk_qffpa_tactic(m, p));
|
||||
MK_SIMPLE_TACTIC_FACTORY(ufbv_fct, mk_ufbv_tactic(m, p));
|
||||
MK_SIMPLE_TACTIC_FACTORY(horn_fct, mk_pdr_tactic(m, p));
|
||||
|
||||
static void init(strategic_solver * s) {
|
||||
s->set_default_tactic(alloc(default_fct));
|
||||
|
@ -77,6 +79,7 @@ static void init(strategic_solver * s) {
|
|||
s->set_tactic_for(symbol("UFBV"), alloc(ufbv_fct));
|
||||
s->set_tactic_for(symbol("BV"), alloc(ufbv_fct));
|
||||
s->set_tactic_for(symbol("QF_FPA"), alloc(qffpa_fct));
|
||||
s->set_tactic_for(symbol("HORN"), alloc(horn_fct));
|
||||
}
|
||||
|
||||
solver * mk_smt_strategic_solver(bool force_tactic) {
|
||||
|
|
|
@ -549,7 +549,7 @@ public:
|
|||
#ifdef _NO_OMP_
|
||||
use_seq = true;
|
||||
#else
|
||||
use_seq = omp_in_parallel();
|
||||
use_seq = 0 != omp_in_parallel();
|
||||
#endif
|
||||
if (use_seq) {
|
||||
// execute tasks sequentially
|
||||
|
@ -677,7 +677,7 @@ public:
|
|||
#ifdef _NO_OMP_
|
||||
use_seq = true;
|
||||
#else
|
||||
use_seq = omp_in_parallel();
|
||||
use_seq = 0 != omp_in_parallel();
|
||||
#endif
|
||||
if (use_seq) {
|
||||
// execute tasks sequentially
|
||||
|
|
Loading…
Reference in a new issue