mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity

reorganizing the code

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-10-25 11:28:03 -07:00
parent 9c057b87d1
commit f57d4b1b19
34 changed files with 602 additions and 181 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ast/normal_forms/nnf.cpp
View file

@ -359,9 +359,9 @@ struct nnf::imp {
void checkpoint() {
cooperate("nnf");
if (memory::get_allocation_size() > m_max_memory)
throw nnf_exception(TACTIC_MAX_MEMORY_MSG);
throw nnf_exception(Z3_MAX_MEMORY_MSG);
if (m_cancel)
throw nnf_exception(TACTIC_CANCELED_MSG);
throw nnf_exception(Z3_CANCELED_MSG);
}
void set_new_child_flag() {

332
src/ast/pattern/database.smt2 Normal file
View file

@ -0,0 +1,332 @@
(declare-fun ?store (Int Int Int) Int)
(declare-fun ?select (Int Int) Int)
(declare-fun ?PO (Int Int) Int)
(declare-fun ?asChild (Int Int) Int)
(declare-fun ?classDown (Int Int) Int)
(declare-fun ?array (Int) Int)
(declare-fun ?elemtype (Int) Int)
(declare-fun ?is (Int Int) Int)
(declare-fun ?cast (Int Int) Int)
(declare-fun ?Object () Int)
(declare-fun ?null () Int)
(declare-fun ?typeof (Int) Int)
(declare-fun ?asElems (Int) Int)
(declare-fun ?isAllocated (Int Int) Int)
(declare-fun ?fClosedTime (Int) Int)
(declare-fun ?eClosedTime (Int) Int)
(declare-fun ?max (Int) Int)
(declare-fun ?asLockSet (Int) Int)
(declare-fun ?isNewArray (Int) Int)
(declare-fun ?classLiteral (Int) Int)
(declare-fun ?Class () Int)
(declare-fun ?alloc () Int)
(declare-fun ?arrayType () Int)
(declare-fun ?f (Int) Int)
(declare-fun ?finv (Int) Int)
(declare-fun ?select2 (Int Int Int) Int)
(declare-fun ?store2 (Int Int Int Int) Int)
(declare-fun ?subtypes (Int Int) Bool)
(declare-fun ?Unbox (Int) Int)
(declare-fun ?UnboxedType (Int) Int)
(declare-fun ?Box (Int Int) Int)
(declare-fun ?System.Object () Int)
(declare-fun ?Smt.true () Int)
(declare-fun ?AsRepField (Int Int) Int)
(declare-fun ?AsPeerField (Int) Int)
(declare-fun ?nullObject () Int)
(declare-fun ?ownerRef_ () Int)
(declare-fun ?ownerFrame_ () Int)
(declare-fun IntsHeap (Int) Int)
(declare-fun ?localinv_ () Int)
(declare-fun ?inv_ () Int)
(declare-fun ?BaseClass_ (Int) Int)
(declare-fun ?typeof_ (Int) Int)
(declare-fun ?PeerGroupPlaceholder_ () Int)
(declare-fun ?ClassRepr (Int) Int)
(declare-fun ?RefArray (Int Int) Int)
(declare-fun Ints_ (Int Int) Int)
(declare-fun ?RefArrayGet (Int Int) Int)
(declare-fun ?elements_ () Int)
(declare-fun ?NonNullRefArray (Int Int) Int)
(declare-fun IntsNotNull_ (Int Int) Int)
(declare-fun ?Rank_ (Int) Int)
(declare-fun ?ValueArray (Int Int) Int)
(declare-fun ?ArrayCategory_ (Int) Int)
(declare-fun ?ArrayCategoryValue_ () Int)
(declare-fun ?ElementType_ (Int) Int)
(declare-fun ?System.Array () Int)
(declare-fun ?allocated_ () Int)
(declare-fun ?StructGet_ (Int Int) Int)
(declare-fun ?AsRangeField (Int Int) Int)
(declare-fun IntsAllocated (Int Int) Int)
(declare-fun IntnRange (Int Int) Bool)
(declare-fun ?isAllocated_ (Int Int) Bool)
(declare-fun ?AsDirectSubClass (Int Int) Int)
(declare-fun ?OneClassDown (Int Int) Int)
(assert (forall ((a Int) (i Int) (e Int))
(!
(= (?select (?store a i e) i) e)
:pattern (?store a i e)
:weight 0)))
(assert (forall ((a Int) (i Int) (j Int) (e Int))
(!
(or (= i j) (= (?select (?store a i e) j) (?select a j)))
:pattern (?select (?store a i e) j)
:weight 0)))
(assert (forall ((t0 Int) (t1 Int) (t2 Int))
(!
(or (not (= (?PO t0 t1) 1))
(not (= (?PO t1 t2) 1))
(= (?PO t0 t2) 1))
:pattern ((?PO t0 t1) (?PO t1 t2)))))
(assert (forall ((t0 Int) (t1 Int))
(!
(or (not (= (?PO t0 t1) 1))
(not (= (?PO t1 t0) 1))
(= t0 t1))
:pattern ((?PO t0 t1) (?PO t1 t0)))))
(assert (forall ((t0 Int) (t1 Int) (t2 Int))
(!
(or (not (= (?PO t0 (?asChild t1 t2)) 1))
(= (?classDown t2 t0) (?asChild t1 t2)))
:pattern (?PO t0 (?asChild t1 t2)))))
(assert (forall ((t Int))
(!
(= (?finv (?f t)) t)
:pattern (?f t))))
(assert (forall ((t0 Int) (t1 Int) )
(!
(iff (= (?PO t0 (?array t1)) 1)
(not (or (not (= t0 (?array (?elemtype t0))))
(not (= (?PO (?elemtype t0) t1) 1)))))
:pattern (?PO t0 (?array t1)))))
(assert (forall ((x Int) (t Int))
(!
(or (not (= (?is x t) 1))
(= (?cast x t) x))
:pattern (?cast x t))))
(assert (forall ((x Int) (t Int))
(!
(or (not (= (?PO t ?Object) 1))
(iff (= (?is x t) 1)
(or (= x ?null)
(= (?PO (?typeof x) t) 1))))
:pattern ((?PO t ?Object) (?is x t)))))
(assert (forall ((e Int) (a Int) (i Int))
(!
(= (?is (?select (?select (?asElems e) a) i)
(?elemtype (?typeof a))) 1)
:pattern (?select (?select (?asElems e) a) i))))
(assert (forall ((x Int) (f Int) (a0 Int))
(!
(or (<= (+ a0 (* -1 (?fClosedTime f))) 0)
(not (= (?isAllocated x a0) 1))
(= (?isAllocated (?select f x) a0) 1))
:pattern (?isAllocated (?select f x) a0))))
(assert (forall ((a Int) (e Int) (i Int) (a0 Int))
(!
(or (<= (+ a0 (* -1 (?eClosedTime e))) 0)
(not (= (?isAllocated a a0) 1))
(= (?isAllocated (?select (?select e a) i) a0) 1))
:pattern (?isAllocated (?select (?select e a) i) a0))))
(assert (forall ((S Int))
(!
(= (?select (?asLockSet S) (?max (?asLockSet S))) 1)
:pattern (?select (?asLockSet S) (?max (?asLockSet S))))))
(assert (forall ((s Int))
(!
(or (not (= 1 (?isNewArray s)))
(= (?PO (?typeof s) ?arrayType) 1))
:pattern (?isNewArray s))))
(assert (forall ((t Int))
(!
(not (or (= (?classLiteral t) ?null)
(not (= (?is (?classLiteral t) ?Class) 1))
(not (= (?isAllocated (?classLiteral t) ?alloc) 1))))
:pattern (?classLiteral t))))
(assert (forall ((A Int) (o Int) (f Int) (v Int))
(!
(= (?select2 (?store2 A o f v) o f) v)
:pattern (?store2 A o f v)
:weight 0)))
(assert (forall ((A Int) (o Int) (f Int) (p Int) (g Int) (v Int))
(!
(or (= o p) (= (?select2 (?store2 A o f v) p g) (?select2 A p g)))
:pattern (?select2 (?store2 A o f v) p g)
:weight 0)))
(assert (forall ((A Int) (o Int) (f Int) (p Int) (g Int) (v Int))
(!
(or (= f g) (= (?select2 (?store2 A o f v) p g) (?select2 A p g)))
:pattern (?select2 (?store2 A o f v) p g)
:weight 0)))
(assert (forall ((t Int) (u Int) (v Int))
(!
(or (not (?subtypes t u))
(not (?subtypes u v))
(?subtypes t v))
:pattern ((?subtypes t u) (?subtypes u v)))))
(assert (forall ((t Int) (u Int))
(!
(or (not (?subtypes t u))
(not (?subtypes u t))
(= t u))
:pattern ((?subtypes t u) (?subtypes u t)))))
(assert (forall ((x Int) (p Int))
(!
(or (not (?subtypes (?UnboxedType (?Box x p)) ?System.Object))
(not (= (?Box x p) p))
(= x p))
:pattern (?subtypes (?UnboxedType (?Box x p)) ?System.Object))))
(assert (forall ((h Int) (o Int) (f Int) (T Int))
(!
(or
(not (= (IntsHeap h) ?Smt.true))
(= (?select2 h o (?AsRepField f T)) ?nullObject)
(not (or (not (= (?select2 h (?select2 h o (?AsRepField f T)) ?ownerRef_) o))
(not (= (?select2 h (?select2 h o (?AsRepField f T)) ?ownerFrame_) T)))))
:pattern (?select2 h o (?AsRepField f T)))))
(assert (forall ((h Int) (o Int) (f Int))
(!
(or
(not (= (IntsHeap h) ?Smt.true))
(= (?select2 h o (?AsPeerField f)) ?nullObject)
(not (or (not (= (?select2 h (?select2 h o (?AsPeerField f)) ?ownerRef_) (?select2 h o ?ownerRef_)))
(not (= (?select2 h (?select2 h o (?AsPeerField f)) ?ownerFrame_) (?select2 h o ?ownerFrame_))))))
:pattern (?select2 h o (?AsPeerField f)))))
(assert (forall ((h Int) (o Int))
(!
(or
(not (= (IntsHeap h) ?Smt.true))
(= (?select2 h o ?ownerFrame_) ?PeerGroupPlaceholder_)
(not (?subtypes (?select2 h (?select2 h o ?ownerRef_) ?inv_) (?select2 h o ?ownerFrame_)))
(= (?select2 h (?select2 h o ?ownerRef_) ?localinv_) (?BaseClass_ (?select2 h o ?ownerFrame_)))
(not (or (not (= (?select2 h o ?inv_) (?typeof_ o)))
(not (= (?select2 h o ?localinv_) (?typeof_ o))))))
:pattern (?subtypes (?select2 h (?select2 h o ?ownerRef_) ?inv_) (?select2 h o ?ownerFrame_)))))
(assert (forall ((T Int) (h Int))
(!
(or (not (= (IntsHeap h) ?Smt.true))
(= (?select2 h (?ClassRepr T) ?ownerFrame_) ?PeerGroupPlaceholder_))
:pattern (?select2 h (?ClassRepr T) ?ownerFrame_))))
(assert (forall ((a Int) (T Int) (i Int) (r Int) (heap Int))
(!
(or (not (= (IntsHeap heap) ?Smt.true))
(not (?subtypes (?typeof_ a) (?RefArray T r)))
(= (Ints_ (?RefArrayGet (?select2 heap a ?elements_) i) T) ?Smt.true))
:pattern ((?subtypes (?typeof_ a) (?RefArray T r)) (?RefArrayGet (?select2 heap a ?elements_) i)))))
(assert (forall ((a Int) (T Int) (r Int))
(!
(or (= a ?nullObject)
(not (?subtypes (?typeof_ a) (?RefArray T r)))
(= (?Rank_ a) r))
:pattern (?subtypes (?typeof_ a) (?RefArray T r)))))
(assert (forall ((T Int) (ET Int) (r Int))
(!
(or (not (?subtypes T (?ValueArray ET r)))
(= (?ArrayCategory_ T) ?ArrayCategoryValue_))
:pattern (?subtypes T (?ValueArray ET r)))))
(assert (forall ((A Int) (r Int) (T Int))
(!
(or
(not (?subtypes T (?RefArray A r)))
(not (or (not (= T (?RefArray (?ElementType_ T) r)))
(not (?subtypes (?ElementType_ T) A)))))
:pattern (?subtypes T (?RefArray A r)))))
(assert (forall ((A Int) (r Int) (T Int))
(!
(or (not (?subtypes T (?ValueArray A r)))
(= T (?ValueArray A r)))
:pattern (?subtypes T (?ValueArray A r)))))
(assert (forall ((A Int) (B Int) (C Int))
(!
(or (not (?subtypes C (?AsDirectSubClass B A)))
(= (?OneClassDown C A) B))
:pattern (?subtypes C (?AsDirectSubClass B A)))))
(assert (forall ((o Int) (T Int))
(!
(iff (= (Ints_ o T) ?Smt.true)
(or (= o ?nullObject)
(?subtypes (?typeof_ o) T)))
:pattern (Ints_ o T))))
(assert (forall ((o Int) (T Int))
(!
(iff (= (IntsNotNull_ o T) ?Smt.true)
(or (= o ?nullObject)
(not (= (Ints_ o T) ?Smt.true))))
:pattern (IntsNotNull_ o T))))
(assert (forall ((h Int) (o Int))
(!
(or (not (= (IntsHeap h) ?Smt.true))
(= o ?nullObject)
(not (?subtypes (?typeof_ o) ?System.Array))
(not (or (not (= (?select2 h o ?inv_) (?typeof_ o)))
(not (= (?select2 h o ?localinv_) (?typeof_ o))))))
:pattern ((?subtypes (?typeof_ o) ?System.Array) (?select2 h o ?inv_)))))
(assert (forall ((h Int) (o Int) (f Int) (T Int))
(!
(or (not (= (IntsHeap h) ?Smt.true))
(IntnRange (?select2 h o (?AsRangeField f T)) T))
:pattern (?select2 h o (?AsRangeField f T)))))
(assert (forall ((h Int) (o Int) (f Int))
(!
(or
(not (= (IntsHeap h) ?Smt.true))
(not (= (?select2 h o ?allocated_) ?Smt.true))
(= (IntsAllocated h (?select2 h o f)) ?Smt.true))
:pattern (IntsAllocated h (?select2 h o f)))))
(assert (forall ((h Int) (s Int) (f Int))
(!
(or (not (= (IntsAllocated h s) ?Smt.true))
(= (IntsAllocated h (?StructGet_ s f)) ?Smt.true))
:pattern (IntsAllocated h (?StructGet_ s f)))))
(assert (forall ((x Int) (f Int) (a0 Int))
(!
(or (<= (+ a0 (* -1 (?fClosedTime f))) 0)
(not (?isAllocated_ x a0))
(?isAllocated_ (?select f x) a0))
:pattern (?isAllocated_ (?select f x) a0))))
(assert (forall ((a Int) (e Int) (i Int) (a0 Int))
(!
(or (<= (+ a0 (* -1 (?eClosedTime e))) 0)
(not (?isAllocated_ a a0))
(?isAllocated_ (?select (?select e a) i) a0))
:pattern (?isAllocated_ (?select (?select e a) i) a0))))
(assert (forall ((e Int) (a Int) (i Int))
(!
(= (?is (?select (?select (?asElems e) a) i)
(?elemtype (?typeof a))) ?Smt.true)
:pattern (?select (?select (?asElems e) a) i))))
(assert (forall ((t0 Int) (t1 Int))
(!
(iff (?subtypes t0 (?array t1))
(not (or (not (= t0 (?array (?elemtype t0))))
(not (?subtypes (?elemtype t0) t1)))))
:pattern (?subtypes t0 (?array t1)))))
(assert (forall ((t0 Int) (t1 Int) (t2 Int))
(!
(or (not (?subtypes t0 (?asChild t1 t2)))
(= (?classDown t2 t0) (?asChild t1 t2)))
:pattern (?subtypes t0 (?asChild t1 t2)))))
(assert (forall ((t0 Int) (t1 Int))
(!
(iff (?subtypes t0 (?array t1))
(not (or (not (= t0 (?array (?elemtype t0))))
(not (?subtypes (?elemtype t0) t1)))))
:pattern (?subtypes t0 (?array t1)))))
(assert (forall ((x Int) (t Int))
(!
(or (not (= (?is x t) ?Smt.true))
(= (?cast x t) x))
:pattern (?cast x t))))
(assert (forall ((x Int) (t Int))
(!
(or (not (?subtypes t ?Object))
(iff (= (?is x t) ?Smt.true)
(or (= x ?null)
(?subtypes (?typeof x) t))))
:pattern ((?subtypes t ?Object) (?is x t)))))
(assert (forall ((e Int) (a Int) (i Int))
(!
(= (?is (?select (?select (?asElems e) a) i)
(?elemtype (?typeof a))) 1)
:pattern (?select (?select (?asElems e) a) i))))

493
src/ast/pattern/expr_pattern_match.cpp Normal file
View file

@ -0,0 +1,493 @@
/*++
Copyright (c) 2007 Microsoft Corporation
Module Name:
ast_pattern_match.cpp
Abstract:
Search for opportune pattern matching utilities.
Author:
Nikolaj Bjorner (nbjorner) 2007-04-10
Leonardo (leonardo)
Notes:
instead of the brute force enumeration of permutations
we can add an instruction 'gate' which copies the ast
into a register and creates another register with the same
term. Matching against a 'gate' is a noop, apart from clearing
the ast in the register. Then on backtracking we know how many
terms were matched from the permutation. It does not make sense
to enumerate all combinations of terms that were not considered, so
skip these.
Also, compilation should re-order terms to fail fast.
--*/
#include"ast.h"
#include"expr_pattern_match.h"
#include"for_each_ast.h"
#include"ast_ll_pp.h"
#include"ast_pp.h"
#include"cmd_context.h"
#include"smt2parser.h"
#include"front_end_params.h"
expr_pattern_match::expr_pattern_match(ast_manager & manager):
m_manager(manager), m_precompiled(manager) {
}
expr_pattern_match::~expr_pattern_match() {
}
bool
expr_pattern_match::match_quantifier(quantifier* qf, app_ref_vector& patterns, unsigned& weight) {
if (m_regs.empty()) {
// HACK: the code crashes if database is empty.
return false;
}
m_regs[0] = qf->get_expr();
for (unsigned i = 0; i < m_precompiled.size(); ++i) {
quantifier* qf2 = m_precompiled[i].get();
if (qf2->is_forall() != qf->is_forall()) {
continue;
}
if (qf2->get_num_decls() != qf->get_num_decls()) {
continue;
}
subst s;
if (match(qf->get_expr(), m_first_instrs[i], s)) {
for (unsigned j = 0; j < qf2->get_num_patterns(); ++j) {
app* p = static_cast<app*>(qf2->get_pattern(j));
expr_ref p_result(m_manager);
instantiate(p, qf->get_num_decls(), s, p_result);
patterns.push_back(to_app(p_result.get()));
}
weight = qf2->get_weight();
return true;
}
}
return false;
}
void
expr_pattern_match::instantiate(expr* a, unsigned num_bound, subst& s, expr_ref& result) {
bound b;
for (unsigned i = 0; i < num_bound; ++i) {
b.insert(m_bound_dom[i], m_bound_rng[i]);
}
inst_proc proc(m_manager, s, b, m_regs);
for_each_ast(proc, a);
expr* v = 0;
proc.m_memoize.find(a, v);
SASSERT(v);
result = v;
}
void
expr_pattern_match::compile(expr* q)
{
SASSERT(q->get_kind() == AST_QUANTIFIER);
quantifier* qf = to_quantifier(q);
unsigned ip = m_instrs.size();
m_first_instrs.push_back(ip);
m_precompiled.push_back(qf);
instr instr(BACKTRACK);
unsigned_vector regs;
ptr_vector<expr> pats;
unsigned max_reg = 1;
subst s;
pats.push_back(qf->get_expr());
regs.push_back(0);
unsigned num_bound = 0;
obj_map<var, unsigned> bound;
while (!pats.empty()) {
unsigned reg = regs.back();
expr* pat = pats.back();
regs.pop_back();
pats.pop_back();
instr.m_pat = pat;
instr.m_next = m_instrs.size()+1;
instr.m_reg = reg;
instr.m_offset = max_reg;
switch(pat->get_kind()) {
case AST_VAR: {
var* b = to_var(pat);
if (bound.find(b, instr.m_num_bound)) {
instr.m_kind = CHECK_BOUND;
}
else {
instr.m_kind = SET_BOUND;
instr.m_num_bound = num_bound;
bound.insert(b, num_bound);
++num_bound;
}
break;
}
case AST_APP: {
unsigned r = 0;
app* app = to_app(pat);
func_decl* d = app->get_decl();
for (unsigned i = 0; i < app->get_num_args(); ++i) {
regs.push_back(max_reg);
pats.push_back(app->get_arg(i));
++max_reg;
}
if (is_var(d)) {
if (s.find(d, r)) {
instr.m_kind = CHECK_VAR;
instr.m_other_reg = r;
}
else {
instr.m_kind = SET_VAR;
s.insert(d, reg);
}
}
else {
if (d->is_associative() && d->is_commutative()) {
instr.m_kind = BIND_AC;
}
else if (d->is_commutative()) {
SASSERT(app->get_num_args() == 2);
instr.m_kind = BIND_C;
}
else {
instr.m_kind = BIND;
}
}
break;
}
default:
instr.m_kind = CHECK_TERM;
break;
}
m_instrs.push_back(instr);
}
if (m_regs.size() <= max_reg) {
m_regs.resize(max_reg+1, 0);
}
if (m_bound_dom.size() <= num_bound) {
m_bound_dom.resize(num_bound+1, 0);
m_bound_rng.resize(num_bound+1, 0);
}
instr.m_kind = YIELD;
m_instrs.push_back(instr);
}
bool
expr_pattern_match::match(expr* a, unsigned init, subst& s)
{
svector<instr> bstack;
instr pc = m_instrs[init];
while (true) {
bool ok = false;
switch(pc.m_kind) {
case YIELD:
// substitution s contains registers with matching declarations.
return true;
case CHECK_TERM:
TRACE("expr_pattern_match", display(tout, pc);
ast_pp(tout, m_regs[pc.m_reg], m_manager) << "\n";);
ok = (pc.m_pat == m_regs[pc.m_reg]);
break;
case SET_VAR:
case CHECK_VAR: {
TRACE("expr_pattern_match", display(tout, pc);
ast_pp(tout, m_regs[pc.m_reg], m_manager) << "\n";);
app* app1 = to_app(pc.m_pat);
a = m_regs[pc.m_reg];
if (a->get_kind() != AST_APP) {
break;
}
app* app2 = to_app(a);
if (app1->get_num_args() != app2->get_num_args()) {
break;
}
if (pc.m_kind == CHECK_VAR &&
to_app(m_regs[pc.m_reg])->get_decl() !=
to_app(m_regs[pc.m_other_reg])->get_decl()) {
break;
}
for (unsigned i = 0; i < app2->get_num_args(); ++i) {
m_regs[pc.m_offset + i] = app2->get_arg(i);
}
if (pc.m_kind == SET_VAR) {
s.insert(app1->get_decl(), pc.m_reg);
}
ok = true;
break;
}
case SET_BOUND: {
TRACE("expr_pattern_match", display(tout, pc);
ast_pp(tout, m_regs[pc.m_reg], m_manager) << "\n";);
a = m_regs[pc.m_reg];
if (a->get_kind() != AST_VAR) {
break;
}
ok = true;
var* var_a = to_var(a);
var* var_p = to_var(pc.m_pat);
// check that the mapping of bound variables remains a bijection.
for (unsigned i = 0; ok && i < pc.m_num_bound; ++i) {
ok = (a != m_bound_rng[i]);
}
if (!ok) {
break;
}
m_bound_dom[pc.m_num_bound] = var_p;
m_bound_rng[pc.m_num_bound] = var_a;
break;
}
case CHECK_BOUND:
TRACE("expr_pattern_match",
tout
<< "check bound "
<< pc.m_num_bound << " " << pc.m_reg;
);
ok = m_bound_rng[pc.m_num_bound] == m_regs[pc.m_reg];
break;
case BIND:
case BIND_AC:
case BIND_C: {
TRACE("expr_pattern_match", display(tout, pc);
tout << mk_pp(m_regs[pc.m_reg],m_manager) << "\n";);
app* app1 = to_app(pc.m_pat);
a = m_regs[pc.m_reg];
if (a->get_kind() != AST_APP) {
break;
}
app* app2 = to_app(a);
if (app1->get_num_args() != app2->get_num_args()) {
break;
}
if (!match_decl(app1->get_decl(), app2->get_decl())) {
break;
}
switch(pc.m_kind) {
case BIND:
for (unsigned i = 0; i < app2->get_num_args(); ++i) {
m_regs[pc.m_offset + i] = app2->get_arg(i);
}
ok = true;
break; // process the next instruction.
case BIND_AC:
// push CHOOSE_AC on the backtracking stack.
bstack.push_back(instr(CHOOSE_AC, pc.m_offset, pc.m_next, app2, 1));
break;
case BIND_C:
// push CHOOSE_C on the backtracking stack.
ok = true;
m_regs[pc.m_offset] = app2->get_arg(0);
m_regs[pc.m_offset+1] = app2->get_arg(1);
bstack.push_back(instr(CHOOSE_C, pc.m_offset, pc.m_next, app2, 2));
break;
default:
break;
}
break;
}
case CHOOSE_C:
ok = true;
SASSERT (pc.m_count == 2);
m_regs[pc.m_offset+1] = pc.m_app->get_arg(0);
m_regs[pc.m_offset] = pc.m_app->get_arg(1);
break;
case CHOOSE_AC: {
ok = true;
app* app2 = pc.m_app;
for (unsigned i = 0; i < app2->get_num_args(); ++i) {
m_regs[pc.m_offset + i] = app2->get_arg(i);
}
// generate the k'th permutation.
unsigned k = pc.m_count;
unsigned fac = 1;
unsigned num_args = pc.m_app->get_num_args();
for (unsigned j = 2; j <= num_args; ++j) {
fac *= (j-1);
SASSERT(((k /fac) % j) + 1 <= j);
std::swap(m_regs[pc.m_offset + j - 1], m_regs[pc.m_offset + j - ((k / fac) % j) - 1]);
}
if (k < fac*num_args) {
bstack.push_back(instr(CHOOSE_AC, pc.m_offset, pc.m_next, app2, k+1));
}
TRACE("expr_pattern_match",
{
tout << "fac: " << fac << " num_args:" << num_args << " k:" << k << "\n";
for (unsigned i = 0; i < num_args; ++i) {
ast_pp(tout, m_regs[pc.m_offset + i], m_manager);
tout << " ";
}
tout << "\n";
});
break;
}
case BACKTRACK:
if (bstack.empty()) {
return false;
}
pc = bstack.back();
bstack.pop_back();
continue; // with the loop.
}
if (ok) {
pc = m_instrs[pc.m_next];
}
else {
TRACE("expr_pattern_match", tout << "backtrack\n";);
pc = m_instrs[0];
}
}
}
bool
expr_pattern_match::match_decl(func_decl const * pat, func_decl const * d) const {
if (pat == d) {
return true;
}
if (pat->get_arity() != d->get_arity()) {
return false;
}
// match families
if (pat->get_family_id() == null_family_id) {
return false;
}
if (d->get_family_id() != pat->get_family_id()) {
return false;
}
if (d->get_decl_kind() != pat->get_decl_kind()) {
return false;
}
if (d->get_num_parameters() != pat->get_num_parameters()) {
return false;
}
for (unsigned i = 0; i < d->get_num_parameters(); ++i) {
if (!(d->get_parameter(i) == pat->get_parameter(i))) {
return false;
}
}
return true;
}
bool
expr_pattern_match::is_var(func_decl* d) {
const char* s = d->get_name().bare_str();
return s && *s == '?';
}
void
expr_pattern_match::initialize(char const * spec_string) {
if (!m_instrs.empty()) {
return;
}
m_instrs.push_back(instr(BACKTRACK));
std::istringstream is(spec_string);
front_end_params p;
cmd_context ctx(p, true, &m_manager);
VERIFY(parse_smt2_commands(ctx, is));
ptr_vector<expr>::const_iterator it = ctx.begin_assertions();
ptr_vector<expr>::const_iterator end = ctx.end_assertions();
for (; it != end; ++it) {
compile(*it);
}
TRACE("expr_pattern_match", display(tout); );
}
void
expr_pattern_match::display(std::ostream& out) const {
for (unsigned i = 0; i < m_instrs.size(); ++i) {
display(out, m_instrs[i]);
}
}
void
expr_pattern_match::display(std::ostream& out, instr const& pc) const {
switch(pc.m_kind) {
case BACKTRACK:
out << "backtrack\n";
break;
case BIND:
out << "bind ";
ast_pp(out, to_app(pc.m_pat)->get_decl(), m_manager) << " ";
ast_pp(out, pc.m_pat, m_manager) << "\n";
out << "next: " << pc.m_next << "\n";
out << "offset: " << pc.m_offset << "\n";
out << "reg: " << pc.m_reg << "\n";
break;
case BIND_AC:
out << "bind_ac ";
ast_pp(out, to_app(pc.m_pat)->get_decl(), m_manager) << " ";
ast_pp(out, pc.m_pat, m_manager) << "\n";
out << "next: " << pc.m_next << "\n";
out << "offset: " << pc.m_offset << "\n";
out << "reg: " << pc.m_reg << "\n";
break;
case BIND_C:
out << "bind_c ";
ast_pp(out, to_app(pc.m_pat)->get_decl(), m_manager) << " ";
ast_pp(out, pc.m_pat, m_manager) << "\n";
out << "next: " << pc.m_next << "\n";
out << "offset: " << pc.m_offset << "\n";
out << "reg: " << pc.m_reg << "\n";
break;
case CHOOSE_AC:
out << "choose_ac\n";
out << "next: " << pc.m_next << "\n";
out << "count: " << pc.m_count << "\n";
break;
case CHOOSE_C:
out << "choose_c\n";
out << "next: " << pc.m_next << "\n";
//out << "reg: " << pc.m_reg << "\n";
break;
case CHECK_VAR:
out << "check_var ";
ast_pp(out, pc.m_pat, m_manager) << "\n";
out << "next: " << pc.m_next << "\n";
out << "reg: " << pc.m_reg << "\n";
out << "other_reg: " << pc.m_other_reg << "\n";
break;
case CHECK_TERM:
out << "check ";
ast_pp(out, pc.m_pat, m_manager) << "\n";
out << "next: " << pc.m_next << "\n";
out << "reg: " << pc.m_reg << "\n";
break;
case YIELD:
out << "yield\n";
break;
case SET_VAR:
out << "set_var ";
ast_pp(out, pc.m_pat, m_manager) << "\n";
out << "next: " << pc.m_next << "\n";
break;
default:
break;
} }
// TBD: fix type overloading.
// TBD: bound number of permutations.
// TBD: forward pruning checks.

148
src/ast/pattern/expr_pattern_match.h Normal file
View file

@ -0,0 +1,148 @@
/*++
Copyright (c) 2007 Microsoft Corporation
Module Name:
expr_pattern_match.h
Abstract:
Search for opportune pattern matching utilities.
Author:
Nikolaj Bjorner (nbjorner) 2007-04-10
Leonardo (leonardo)
Notes:
--*/
#ifndef _EXPR_PATTERN_MATCH_H_
#define _EXPR_PATTERN_MATCH_H_
#include"ast.h"
#include"map.h"
#include"front_end_params.h"
class expr_pattern_match {
enum instr_kind {
BACKTRACK,
BIND,
BIND_AC,
BIND_C,
CHOOSE_AC,
CHOOSE_C,
SET_VAR,
CHECK_VAR,
CHECK_TERM,
SET_BOUND,
CHECK_BOUND,
YIELD,
};
struct instr {
instr(instr_kind k) : m_kind(k) {}
instr(instr_kind k, unsigned o, unsigned next, app* app, unsigned count):
m_kind(k), m_offset(o), m_next(next), m_app(app), m_count(count) {}
instr_kind m_kind;
unsigned m_offset;
unsigned m_next;
app* m_app;
expr* m_pat;
unsigned m_reg;
unsigned m_other_reg;
unsigned m_count;
unsigned m_num_bound;
};
typedef obj_map<func_decl, unsigned> subst;
typedef obj_map<var, var*> bound;
struct inst_proc {
ast_manager& m_manager;
expr_ref_vector m_pinned;
subst& m_subst;
bound& m_bound;
obj_map<expr, expr*> m_memoize;
ptr_vector<expr>& m_regs;
inst_proc(ast_manager& m, subst& s, bound& b, ptr_vector<expr>& regs) :
m_manager(m), m_pinned(m), m_subst(s), m_bound(b), m_regs(regs) {}
void operator()(ast* a) {
}
void operator()(expr* a) {
m_memoize.insert(a, a);
}
void operator()(var* v) {
var* b = 0;
if (m_bound.find(v, b)) {
m_memoize.insert(v, b);
}
else {
UNREACHABLE();
}
}
void operator()(app * n) {
unsigned r;
ptr_vector<expr> args;
unsigned num_args = n->get_num_args();
func_decl * decl = n->get_decl();
expr* result;
if (m_subst.find(decl, r)) {
decl = to_app(m_regs[r])->get_decl();
}
for (unsigned i = 0; i < num_args; ++i) {
expr* arg = 0;
if (m_memoize.find(n->get_arg(i), arg)) {
SASSERT(arg);
args.push_back(arg);
}
else {
UNREACHABLE();
}
}
if (m_manager.is_pattern(n)) {
result = m_manager.mk_pattern(num_args, reinterpret_cast<app**>(args.c_ptr()));
}
else {
result = m_manager.mk_app(decl, num_args, args.c_ptr());
}
m_pinned.push_back(result);
m_memoize.insert(n, result);
return;
}
};
ast_manager & m_manager;
quantifier_ref_vector m_precompiled;
unsigned_vector m_first_instrs;
svector<instr> m_instrs;
ptr_vector<expr> m_regs;
ptr_vector<var> m_bound_dom;
ptr_vector<var> m_bound_rng;
public:
expr_pattern_match(ast_manager & manager);
~expr_pattern_match();
virtual bool match_quantifier(quantifier * qf, app_ref_vector & patterns, unsigned & weight);
virtual void initialize(char const * database);
void display(std::ostream& out) const;
private:
void instantiate(expr* a, unsigned num_bound, subst& s, expr_ref& result);
void compile(expr* q);
bool match(expr* a, unsigned init, subst& s);
bool match_decl(func_decl const * pat, func_decl const * d) const;
bool is_var(func_decl* d);
void display(std::ostream& out, instr const& pc) const;
};
#endif

13
src/ast/pattern/pattern_inference.cpp
View file

@ -87,7 +87,7 @@ bool smaller_pattern::operator()(unsigned num_bindings, expr * p1, expr * p2) {
return process(p1, p2);
}
pattern_inference::pattern_inference(ast_manager & m, pattern_inference_params & params, pattern_database * db):
pattern_inference::pattern_inference(ast_manager & m, pattern_inference_params & params):
simplifier(m),
m_params(params),
m_bfid(m.get_basic_family_id()),
@ -99,7 +99,7 @@ pattern_inference::pattern_inference(ast_manager & m, pattern_inference_params &
m_pattern_weight_lt(m_candidates_info),
m_collect(m, *this),
m_contains_subpattern(*this),
m_database(db) {
m_database(m) {
if (params.m_pi_arith == AP_NO)
register_forbidden_family(m_afid);
enable_ac_support(false);
@ -574,6 +574,8 @@ void pattern_inference::mk_patterns(unsigned num_bindings,
m_candidates.reset();
}
#include"database.h" // defines g_pattern_database
void pattern_inference::reduce1_quantifier(quantifier * q) {
TRACE("pattern_inference", tout << "processing:\n" << mk_pp(q, m_manager) << "\n";);
if (!q->is_forall()) {
@ -582,11 +584,12 @@ void pattern_inference::reduce1_quantifier(quantifier * q) {
}
int weight = q->get_weight();
if (m_database) {
if (m_params.m_pi_use_database) {
m_database.initialize(g_pattern_database);
app_ref_vector new_patterns(m_manager);
unsigned new_weight;
if (m_database->match_quantifier(q, new_patterns, new_weight)) {
if (m_database.match_quantifier(q, new_patterns, new_weight)) {
#ifdef Z3DEBUG
for (unsigned i = 0; i < new_patterns.size(); i++) { SASSERT(is_well_sorted(m_manager, new_patterns.get(i))); }
#endif

12
src/ast/pattern/pattern_inference.h
View file

@ -28,13 +28,7 @@ Revision History:
#include"obj_hashtable.h"
#include"obj_pair_hashtable.h"
#include"map.h"
class pattern_database {
public:
virtual ~pattern_database() {}
virtual void initialize(char const * smt_patterns) = 0;
virtual bool match_quantifier(quantifier * qf, app_ref_vector & patterns, unsigned & weight) = 0;
};
#include"expr_pattern_match.h"
/**
\brief A pattern p_1 is smaller than a pattern p_2 iff
@ -195,7 +189,7 @@ class pattern_inference : public simplifier {
};
ptr_vector<pre_pattern> m_pre_patterns;
pattern_database * m_database;
expr_pattern_match m_database;
void candidates2unary_patterns(ptr_vector<app> const & candidate_patterns,
ptr_vector<app> & remaining_candidate_patterns,
@ -223,7 +217,7 @@ class pattern_inference : public simplifier {
virtual void reduce1_quantifier(quantifier * q);
public:
pattern_inference(ast_manager & m, pattern_inference_params & params, pattern_database * db);
pattern_inference(ast_manager & m, pattern_inference_params & params);
void register_forbidden_family(family_id fid) {
SASSERT(fid != m_bfid);

6
src/ast/rewriter/rewriter.h
View file

@ -246,17 +246,17 @@ protected:
// check maximum number of scopes
void check_max_scopes() const {
if (m_cfg.max_scopes_exceeded(this->m_scopes.size()))
throw rewriter_exception(TACTIC_MAX_SCOPES_MSG);
throw rewriter_exception(Z3_MAX_SCOPES_MSG);
}
// check maximum size of the frame stack
void check_max_frames() const {
if (m_cfg.max_frames_exceeded(frame_stack().size()))
throw rewriter_exception(TACTIC_MAX_FRAMES_MSG);
throw rewriter_exception(Z3_MAX_FRAMES_MSG);
}
// check maximum number of rewriting steps
void check_max_steps() const {
if (m_cfg.max_steps_exceeded(m_num_steps))
throw rewriter_exception(TACTIC_MAX_STEPS_MSG);
throw rewriter_exception(Z3_MAX_STEPS_MSG);
}
// If pre_visit returns false, then t children are not visited/rewritten.

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

@ -577,7 +577,7 @@ void rewriter_tpl<Config>::resume_core(expr_ref & result, proof_ref & result_pr)
SASSERT(!frame_stack().empty());
while (!frame_stack().empty()) {
if (m_cancel)
throw rewriter_exception(TACTIC_CANCELED_MSG);
throw rewriter_exception(Z3_CANCELED_MSG);
SASSERT(!ProofGen || result_stack().size() == result_pr_stack().size());
frame & fr = frame_stack().back();
expr * t = fr.m_curr;

7
src/ast/rewriter/rewriter_types.h
View file

@ -19,7 +19,8 @@ Notes:
#ifndef _REWRITER_TYPES_H_
#define _REWRITER_TYPES_H_
#include"tactic_exception.h"
#include"z3_exception.h"
#include"common_msgs.h"
/**
\brief Builtin rewrite result status
@ -43,9 +44,9 @@ inline br_status unsigned2br_status(unsigned u) {
return r;
}
class rewriter_exception : public tactic_exception {
class rewriter_exception : public default_exception {
public:
rewriter_exception(char const * msg):tactic_exception(msg) {}
rewriter_exception(char const * msg):default_exception(msg) {}
};
#endif

2
src/ast/rewriter/th_rewriter.cpp
View file

@ -96,7 +96,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
bool max_steps_exceeded(unsigned num_steps) const {
cooperate("simplifier");
if (memory::get_allocation_size() > m_max_memory)
throw rewriter_exception(TACTIC_MAX_MEMORY_MSG);
throw rewriter_exception(Z3_MAX_MEMORY_MSG);
return num_steps > m_max_steps;
}