mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

checkpoint

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-10-21 21:50:58 -07:00
parent 80b2df3621
commit 78b11ccd8e
23 changed files with 58 additions and 19 deletions
Download patch file Download diff file Expand all files Collapse all files

494
src/api/expr_pattern_match.cpp Normal file
View file

@ -0,0 +1,494 @@
/*++
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"smtparser.h"
#include"for_each_ast.h"
#include"ast_ll_pp.h"
#include"ast_pp.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));
smtlib::parser* parser = smtlib::parser::create(m_manager);
parser->initialize_smtlib();
if (!parser->parse_string(spec_string)) {
UNREACHABLE();
}
smtlib::benchmark* bench = parser->get_benchmark();
smtlib::theory::expr_iterator it = bench->begin_formulas();
smtlib::theory::expr_iterator end = bench->end_formulas();
for (; it != end; ++it) {
compile(*it);
}
dealloc(parser);
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.

149
src/api/expr_pattern_match.h Normal file
View file

@ -0,0 +1,149 @@
/*++
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"
#include"pattern_inference.h"
class expr_pattern_match : public pattern_database {
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

252
src/api/smtlib.cpp Normal file
View file

@ -0,0 +1,252 @@
#include"smtlib.h"
#include"ast_pp.h"
#include"ast_smt2_pp.h"
#ifdef _WINDOWS
#ifdef ARRAYSIZE
#undef ARRAYSIZE
#endif
#include <windows.h>
#include <strsafe.h>
#endif
#include <iostream>
using namespace smtlib;
// --------------------------------------------------------------------------
// symtable
symtable::~symtable() {
reset();
}
void symtable::reset() {
svector<ptr_vector<func_decl>*> range;
m_ids.get_range(range);
for (unsigned i = 0; i < range.size(); ++i) {
ptr_vector<func_decl> const & v = *range[i];
for (unsigned j = 0; j < v.size(); ++j) {
m_manager.dec_ref(v[j]);
}
dealloc(range[i]);
}
m_ids.reset();
ptr_vector<sort> sorts;
m_sorts1.get_range(sorts);
for (unsigned i = 0; i < sorts.size(); ++i) {
m_manager.dec_ref(sorts[i]);
}
m_sorts1.reset();
ptr_vector<sort_builder> sort_builders;
m_sorts.get_range(sort_builders);
for (unsigned i = 0; i < sort_builders.size(); ++i) {
dealloc(sort_builders[i]);
}
m_sorts.reset();
}
void symtable::insert(symbol s, func_decl * d) {
ptr_vector<func_decl>* decls = 0;
m_manager.inc_ref(d);
if (!m_ids.find(s, decls)) {
SASSERT(!decls);
decls = alloc(ptr_vector<func_decl>);
decls->push_back(d);
m_ids.insert(s, decls);
}
else {
SASSERT(decls);
if ((*decls)[0] != d) {
decls->push_back(d);
}
else {
m_manager.dec_ref(d);
}
}
}
bool symtable::find1(symbol s, func_decl*& d) {
ptr_vector<func_decl>* decls = 0;
if (!m_ids.find(s, decls)) {
SASSERT(!decls);
return false;
}
SASSERT(decls && !decls->empty());
d = (*decls)[0];
return true;
}
bool symtable::find_overload(symbol s, ptr_vector<sort> const & dom, func_decl * & d) {
ptr_vector<func_decl>* decls = 0;
d = 0;
if (!m_ids.find(s, decls)) {
SASSERT(!decls);
return false;
}
SASSERT(decls);
for (unsigned i = 0; i < decls->size(); ++i) {
func_decl* decl = (*decls)[i];
if (decl->is_associative() && decl->get_arity() > 0) {
for (unsigned j = 0; j < dom.size(); ++j) {
if (dom[j] != decl->get_domain(0)) {
goto try_next;
}
}
d = decl;
return true;
}
if (decl->get_arity() != dom.size()) {
goto try_next;
}
for (unsigned j = 0; j < decl->get_arity(); ++j) {
if (decl->get_domain(j) != dom[j]) {
goto try_next;
}
}
d = decl;
return true;
try_next:
if (decl->get_family_id() == m_manager.get_basic_family_id() && decl->get_decl_kind() == OP_DISTINCT) {
// we skip type checking for 'distinct'
d = decl;
return true;
}
}
return false;
}
// Store in result the func_decl that are not attached to any family id.
// That is, the uninterpreted constants and function declarations.
void symtable::get_func_decls(ptr_vector<func_decl> & result) const {
svector<ptr_vector<func_decl>*> tmp;
m_ids.get_range(tmp);
svector<ptr_vector<func_decl>*>::const_iterator it = tmp.begin();
svector<ptr_vector<func_decl>*>::const_iterator end = tmp.end();
for (; it != end; ++it) {
ptr_vector<func_decl> * curr = *it;
if (curr) {
ptr_vector<func_decl>::const_iterator it2 = curr->begin();
ptr_vector<func_decl>::const_iterator end2 = curr->end();
for (; it2 != end2; ++it2) {
func_decl * d = *it2;
if (d && d->get_family_id() == null_family_id) {
result.push_back(d);
}
}
}
}
}
void symtable::insert(symbol s, sort_builder* sb) {
m_sorts.insert(s, sb);
}
bool symtable::lookup(symbol s, sort_builder*& sb) {
return m_sorts.find(s, sb);
}
void symtable::push_sort(symbol name, sort* srt) {
m_sorts.begin_scope();
sort_builder* sb = alloc(basic_sort_builder,srt);
m_sorts.insert(name, sb);
m_sorts_trail.push_back(sb);
}
void symtable::pop_sorts(unsigned num_sorts) {
while (num_sorts > 0) {
dealloc(m_sorts_trail.back());
m_sorts_trail.pop_back();
m_sorts.end_scope();
}
}
void symtable::get_sorts(ptr_vector<sort>& result) const {
vector<sort*,false> tmp;
m_sorts1.get_range(tmp);
for (unsigned i = 0; i < tmp.size(); ++i) {
if (tmp[i]->get_family_id() == null_family_id) {
result.push_back(tmp[i]);
}
}
}
// --------------------------------------------------------------------------
// theory
func_decl * theory::declare_func(symbol const & id, sort_ref_buffer & domain, sort * range,
bool is_assoc, bool is_comm, bool is_inj) {
func_decl * decl = m_ast_manager.mk_func_decl(id, domain.size(), domain.c_ptr(), range,
is_assoc, is_comm, is_inj);
m_symtable.insert(id, decl);
m_asts.push_back(decl);
return decl;
}
sort * theory::declare_sort(symbol const & id) {
sort * decl = m_ast_manager.mk_sort(id);
m_symtable.insert(id, decl);
m_asts.push_back(decl);
return decl;
}
bool theory::get_func_decl(symbol id, func_decl * & decl) {
return m_symtable.find1(id, decl);
}
bool theory::get_sort(symbol id, sort* & s) {
return m_symtable.find(id, s);
}
bool theory::get_const(symbol id, expr * & term) {
func_decl* decl = 0;
if (!get_func_decl(id,decl)) {
return false;
}
if (decl->get_arity() != 0) {
return false;
}
term = m_ast_manager.mk_const(decl);
m_asts.push_back(term);
return true;
}
void benchmark::display_as_smt2(std::ostream & out) const {
if (m_logic != symbol::null)
out << "(set-logic " << m_logic << ")\n";
out << "(set-info :smt-lib-version 2.0)\n";
out << "(set-info :status ";
switch (m_status) {
case SAT: out << "sat"; break;
case UNSAT: out << "unsat"; break;
default: out << "unknown"; break;
}
out << ")\n";
#if 0
ast_manager & m = m_ast_manager;
ptr_vector<func_decl> decls;
m_symtable.get_func_decls(decls);
ptr_vector<func_decl>::const_iterator it = decls.begin();
ptr_vector<func_decl>::const_iterator end = decls.end();
for (; it != end; ++it) {
func_decl * f = *it;
out << "(declare-fun " << f->get_name() << " (";
for (unsigned i = 0; i < f->get_arity(); i++) {
if (i > 0) out << " ";
out << mk_ismt2_pp(f->get_domain(i), m);
}
out << ") " << mk_ismt2_pp(f->get_range(), m);
out << ")\n";
}
#endif
}

232
src/api/smtlib.h Normal file
View file

@ -0,0 +1,232 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
smtlib.h
Abstract:
SMT library utilities
Author:
Nikolaj Bjorner (nbjorner) 2006-09-29
Revision History:
--*/
#ifndef _SMTLIB_H_
#define _SMTLIB_H_
#include "ast.h"
#include "symbol_table.h"
#include "map.h"
#include "arith_decl_plugin.h"
namespace smtlib {
class sort_builder {
public:
virtual ~sort_builder() {}
virtual bool apply(unsigned num_params, parameter const* params, sort_ref& result) = 0;
virtual char const* error_message() { return ""; }
};
class basic_sort_builder : public sort_builder {
sort* m_sort;
public:
basic_sort_builder(sort* s) : m_sort(s) {}
virtual bool apply(unsigned np, parameter const*, sort_ref& result) {
result = m_sort;
return m_sort && np != 0;
}
};
class symtable {
ast_manager& m_manager;
symbol_table<sort*> m_sorts1;
symbol_table<sort_builder*> m_sorts;
ptr_vector<sort_builder> m_sorts_trail;
symbol_table<ptr_vector<func_decl>* > m_ids;
public:
symtable(ast_manager& m): m_manager(m) {}
~symtable();
void reset();
void insert(symbol s, func_decl * d);
bool find(symbol s, ptr_vector<func_decl> * & decls) {
return m_ids.find(s, decls);
}
bool find1(symbol s, func_decl * & d);
bool find_overload(symbol s, ptr_vector<sort> const & dom, func_decl * & d);
void insert(symbol s, sort * d) {
sort * d2;
if (m_sorts1.find(s, d2)) {
m_manager.dec_ref(d2);
}
m_manager.inc_ref(d);
m_sorts1.insert(s, d);
}
bool find(symbol s, sort * & d) {
return m_sorts1.find(s, d);
}
void insert(symbol s, sort_builder* sb);
bool lookup(symbol s, sort_builder*& sb);
void push_sort(symbol s, sort*);
void pop_sorts(unsigned num_sorts);
void get_func_decls(ptr_vector<func_decl> & result) const;
void get_sorts(ptr_vector<sort>& result) const;
};
class theory {
public:
typedef ptr_vector<expr>::const_iterator expr_iterator;
theory(ast_manager & ast_manager, symbol const& name):
m_name(name),
m_ast_manager(ast_manager),
m_symtable(ast_manager),
m_asts(ast_manager)
{}
virtual ~theory() {}
symtable * get_symtable() { return &m_symtable; }
void insert(sort * s) { m_symtable.insert(s->get_name(), s); }
void insert(func_decl * c) { m_symtable.insert(c->get_name(), c); }
func_decl * declare_func(symbol const & id, sort_ref_buffer & domain, sort * range,
bool is_assoc, bool is_comm, bool is_inj);
sort * declare_sort(symbol const & id);
void add_axiom(expr * axiom) {
m_asts.push_back(axiom);
m_axioms.push_back(axiom);
}
expr_iterator begin_axioms() const {
return m_axioms.begin();
}
unsigned get_num_axioms() const {
return m_axioms.size();
}
expr * const * get_axioms() const {
return m_axioms.c_ptr();
}
expr_iterator end_axioms() const {
return m_axioms.end();
}
void add_assumption(expr * axiom) {
m_asts.push_back(axiom);
m_assumptions.push_back(axiom);
}
unsigned get_num_assumptions() const {
return m_assumptions.size();
}
expr * const * get_assumptions() const {
return m_assumptions.c_ptr();
}
bool get_func_decl(symbol, func_decl*&);
bool get_sort(symbol, sort*&);
bool get_const(symbol, expr*&);
void set_name(symbol const& name) { m_name = name; }
symbol const get_name() const { return m_name; }
protected:
symbol m_name;
ast_manager& m_ast_manager;
ptr_vector<expr> m_axioms;
ptr_vector<expr> m_assumptions;
symtable m_symtable;
ast_ref_vector m_asts;
private:
theory& operator=(theory const&);
theory(theory const&);
};
class benchmark : public theory {
public:
enum status {
UNKNOWN,
SAT,
UNSAT
};
benchmark(ast_manager & ast_manager, symbol const & name) :
theory(ast_manager, name),
m_status(UNKNOWN) {}
virtual ~benchmark() {}
status get_status() const { return m_status; }
void set_status(status status) { m_status = status; }
symbol get_logic() const {
if (m_logic == symbol::null) {
return symbol("ALL");
}
return m_logic;
}
void set_logic(symbol const & s) { m_logic = s; }
unsigned get_num_formulas() const {
return m_formulas.size();
}
expr_iterator begin_formulas() const {
return m_formulas.begin();
}
expr_iterator end_formulas() const {
return m_formulas.end();
}
void add_formula(expr * formula) {
m_asts.push_back(formula);
m_formulas.push_back(formula);
}
void display_as_smt2(std::ostream & out) const;
private:
status m_status;
symbol m_logic;
ptr_vector<expr> m_formulas;
};
};
#endif

117
src/api/smtlib_solver.cpp Normal file
View file

@ -0,0 +1,117 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
smtlib_solver.cpp
Abstract:
SMT based solver.
Author:
Nikolaj Bjorner (nbjorner) 2006-11-3.
Revision History:
--*/
#include"smtparser.h"
#include"smtlib_solver.h"
#include"warning.h"
#include"ast_pp.h"
#include"ast_ll_pp.h"
#include"well_sorted.h"
#include"spc_prover.h"
#include"model.h"
#include"model_v2_pp.h"
// #include"expr2dot.h"
#include"solver.h"
#include"smt_strategic_solver.h"
#include"cmd_context.h"
namespace smtlib {
solver::solver(front_end_params & params):
m_ast_manager(params.m_proof_mode, params.m_trace_stream),
m_params(params),
m_ctx(0),
m_parser(parser::create(m_ast_manager, params.m_ignore_user_patterns)),
m_error_code(0) {
m_parser->initialize_smtlib();
}
solver::~solver() {
if (m_ctx)
dealloc(m_ctx);
}
bool solver::solve_smt(char const * benchmark_file) {
IF_VERBOSE(100, verbose_stream() << "parsing...\n";);
if (!m_parser->parse_file(benchmark_file)) {
if (benchmark_file) {
warning_msg("could not parse file '%s'.", benchmark_file);
}
else {
warning_msg("could not parse input stream.");
}
m_error_code = ERR_PARSER;
return false;
}
benchmark * benchmark = m_parser->get_benchmark();
solve_benchmark(*benchmark);
return true;
}
bool solver::solve_smt_string(char const * benchmark_string) {
if (!m_parser->parse_string(benchmark_string)) {
warning_msg("could not parse string '%s'.", benchmark_string);
return false;
}
benchmark * benchmark = m_parser->get_benchmark();
solve_benchmark(*benchmark);
return true;
}
void solver::display_statistics() {
if (m_ctx)
m_ctx->display_statistics();
}
void solver::solve_benchmark(benchmark & benchmark) {
if (benchmark.get_num_formulas() == 0) {
// Hack: it seems SMT-LIB allow benchmarks without any :formula
benchmark.add_formula(m_ast_manager.mk_true());
}
m_ctx = alloc(cmd_context, m_params, true, &m_ast_manager, benchmark.get_logic());
m_ctx->set_solver(mk_smt_strategic_solver(*m_ctx));
theory::expr_iterator fit = benchmark.begin_formulas();
theory::expr_iterator fend = benchmark.end_formulas();
for (; fit != fend; ++fit)
solve_formula(benchmark, *fit);
}
void solver::solve_formula(benchmark const & benchmark, expr * f) {
IF_VERBOSE(100, verbose_stream() << "starting...\n";);
m_ctx->reset();
for (unsigned i = 0; i < benchmark.get_num_axioms(); i++)
m_ctx->assert_expr(benchmark.get_axioms()[i]);
m_ctx->assert_expr(f);
m_ctx->check_sat(benchmark.get_num_assumptions(), benchmark.get_assumptions());
check_sat_result * r = m_ctx->get_check_sat_result();
if (r != 0) {
proof * pr = r->get_proof();
if (pr != 0 && m_params.m_display_proof)
std::cout << mk_ll_pp(pr, m_ast_manager, false, false);
model_ref md;
if (r->status() != l_false) r->get_model(md);
if (md.get() != 0 && m_params.m_model) {
model_v2_pp(std::cout, *(md.get()), m_params.m_model_partial);
}
}
else {
m_error_code = ERR_UNKNOWN_RESULT;
}
}
};

48
src/api/smtlib_solver.h Normal file
View file

@ -0,0 +1,48 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
smtlib_solver.h
Abstract:
SMT based solver.
Author:
Nikolaj Bjorner (nbjorner) 2006-11-3.
Revision History:
--*/
#ifndef _SMTLIB_SOLVER_H_
#define _SMTLIB_SOLVER_H_
#include"smtparser.h"
#include"front_end_params.h"
#include"lbool.h"
class cmd_context;
namespace smtlib {
class solver {
ast_manager m_ast_manager;
front_end_params & m_params;
cmd_context * m_ctx;
scoped_ptr<parser> m_parser;
unsigned m_error_code;
public:
solver(front_end_params & params);
~solver();
bool solve_smt(char const * benchmark_file);
bool solve_smt_string(char const * benchmark_string);
void display_statistics();
unsigned get_error_code() const { return m_error_code; }
private:
void solve_benchmark(benchmark & benchmark);
void solve_formula(benchmark const & benchmark, expr * f);
};
};
#endif

5320
src/api/smtparser.cpp Normal file
View file

File diff suppressed because it is too large Load diff

51
src/api/smtparser.h Normal file
View file

@ -0,0 +1,51 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
smtparser.h
Abstract:
SMT parsing utilities
Author:
Nikolaj Bjorner (nbjorner) 2006-09-25
Revision History:
--*/
#ifndef _SMT_PARSER_H_
#define _SMT_PARSER_H_
#include "ast.h"
#include "vector.h"
#include "smtlib.h"
#include "z3.h"
#include <iostream>
namespace smtlib {
class parser {
public:
static parser * create(ast_manager & ast_manager, bool ignore_user_patterns = false);
virtual ~parser() {}
virtual void add_builtin_op(char const *, family_id fid, decl_kind kind) = 0;
virtual void add_builtin_type(char const *, family_id fid, decl_kind kind) = 0;
virtual void initialize_smtlib() = 0;
virtual void set_error_stream(std::ostream& strm) = 0;
virtual bool parse_file(char const * path) = 0;
virtual bool parse_string(char const * string) = 0;
virtual bool parse_commands(Z3_context ctx, std::istream& is, std::ostream& os) = 0;
virtual benchmark * get_benchmark() = 0;
};
};
#endif