1
2 /*++
3 Copyright (c) 2015 Microsoft Corporation
4
5 --*/
6
7 #include <string>
8 #include <cstring>
9 #include <list>
10 #include <vector>
11 #include <set>
12 #include <map>
13 #include <signal.h>
14 #include <time.h>
15 #include <iostream>
16 #include <fstream>
17 #include <limits>
18 #include <string.h>
19 #include <cstdlib>
20 #include "z3++.h"
21
22 struct alloc_region {
23 std::list<char*> m_alloc;
24
allocatealloc_region25 void * allocate(size_t s) {
26 char * res = new char[s];
27 m_alloc.push_back(res);
28 return res;
29 }
30
~alloc_regionalloc_region31 ~alloc_region() {
32 std::list<char*>::iterator it = m_alloc.begin(), end = m_alloc.end();
33 for (; it != end; ++it) {
34 delete *it;
35 }
36 }
37 };
38
39 template<typename T>
40 class flet {
41 T & m_ref;
42 T m_old;
43 public:
flet(T & x,T const & y)44 flet(T& x, T const& y): m_ref(x), m_old(x) { x = y; }
~flet()45 ~flet() { m_ref = m_old; }
46 };
47
48 struct symbol_compare {
operator ()symbol_compare49 bool operator()(z3::symbol const& s1, z3::symbol const& s2) const {
50 return s1 < s2;
51 };
52 };
53
54
55 template <typename T>
56 struct symbol_table {
57 typedef std::map<z3::symbol, T> map;
58 map m_map;
59
insertsymbol_table60 void insert(z3::symbol s, T val) {
61 m_map.insert(std::pair<z3::symbol, T>(s, val));
62 }
63
findsymbol_table64 bool find(z3::symbol const& s, T& val) {
65 typename map::iterator it = m_map.find(s);
66 if (it == m_map.end()) {
67 return false;
68 }
69 else {
70 val = it->second;
71 return true;
72 }
73 }
74 };
75
76
77 typedef std::set<z3::symbol, symbol_compare> symbol_set;
78
79
80 struct named_formulas {
81 std::vector<z3::expr> m_formulas;
82 std::vector<std::string> m_names;
83 std::vector<std::string> m_files;
84 bool m_has_conjecture;
85
named_formulasnamed_formulas86 named_formulas(): m_has_conjecture(false) {}
87
push_backnamed_formulas88 void push_back(z3::expr fml, char const * name, char const* file) {
89 m_formulas.push_back(fml);
90 m_names.push_back(name);
91 m_files.push_back(file);
92 }
93
set_has_conjecturenamed_formulas94 void set_has_conjecture() {
95 m_has_conjecture = true;
96 }
97
has_conjecturenamed_formulas98 bool has_conjecture() const {
99 return m_has_conjecture;
100 }
101 };
102
operator new(size_t s,alloc_region & r)103 inline void * operator new(size_t s, alloc_region & r) { return r.allocate(s); }
104
operator new[](size_t s,alloc_region & r)105 inline void * operator new[](size_t s, alloc_region & r) { return r.allocate(s); }
106
operator delete(void *,alloc_region &)107 inline void operator delete(void *, alloc_region & ) { /* do nothing */ }
108
operator delete[](void *,alloc_region &)109 inline void operator delete[](void *, alloc_region & ) { /* do nothing */ }
110
111 struct failure_ex {
112 std::string msg;
failure_exfailure_ex113 failure_ex(char const* m):msg(m) {}
114 };
115
116
117 extern char* tptp_lval[];
118 extern int yylex();
119
strdup(alloc_region & r,char const * s)120 static char* strdup(alloc_region& r, char const* s) {
121 size_t l = strlen(s) + 1;
122 char* result = new (r) char[l];
123 memcpy(result, s, l);
124 return result;
125 }
126
127 class TreeNode {
128 char const* m_symbol;
129 int m_symbol_index;
130 TreeNode** m_children;
131
132 public:
TreeNode(alloc_region & r,char const * sym,TreeNode * A,TreeNode * B,TreeNode * C,TreeNode * D,TreeNode * E,TreeNode * F,TreeNode * G,TreeNode * H,TreeNode * I,TreeNode * J)133 TreeNode(alloc_region& r, char const* sym,
134 TreeNode* A, TreeNode* B, TreeNode* C, TreeNode* D, TreeNode* E,
135 TreeNode* F, TreeNode* G, TreeNode* H, TreeNode* I, TreeNode* J):
136 m_symbol(strdup(r, sym)),
137 m_symbol_index(-1) {
138 m_children = new (r) TreeNode*[10];
139 m_children[0] = A;
140 m_children[1] = B;
141 m_children[2] = C;
142 m_children[3] = D;
143 m_children[4] = E;
144 m_children[5] = F;
145 m_children[6] = G;
146 m_children[7] = H;
147 m_children[8] = I;
148 m_children[9] = J;
149
150 }
151
symbol() const152 char const* symbol() const { return m_symbol; }
children() const153 TreeNode *const* children() const { return m_children; }
child(unsigned i) const154 TreeNode* child(unsigned i) const { return m_children[i]; }
index() const155 int index() const { return m_symbol_index; }
156
set_index(int idx)157 void set_index(int idx) { m_symbol_index = idx; }
158 };
159
MkToken(alloc_region & r,char const * token,int symbolIndex)160 TreeNode* MkToken(alloc_region& r, char const* token, int symbolIndex) {
161 TreeNode* ss;
162 char* symbol = tptp_lval[symbolIndex];
163 ss = new (r) TreeNode(r, symbol, NULL,NULL,NULL,NULL,NULL,NULL,NULL,NULL,NULL,NULL);
164 ss->set_index(symbolIndex);
165 return ss;
166 }
167
168
169 // ------------------------------------------------------
170 // Build Z3 formulas.
171
172 class env {
173 z3::context& m_context;
174 z3::expr_vector m_bound; // vector of bound constants.
175 z3::sort m_univ;
176 symbol_table<z3::func_decl> m_decls;
177 symbol_table<z3::sort> m_defined_sorts;
178 static std::vector<TreeNode*>* m_nodes;
179 static alloc_region* m_region;
180 char const* m_filename;
181
182
183 enum binary_connective {
184 IFF,
185 IMPLIES,
186 IMPLIED,
187 LESS_TILDE_GREATER,
188 TILDE_VLINE
189 };
190
mk_error(TreeNode * f,char const * msg)191 void mk_error(TreeNode* f, char const* msg) {
192 std::ostringstream strm;
193 strm << "expected: " << msg << "\n";
194 strm << "got: " << f->symbol();
195 throw failure_ex(strm.str().c_str());
196 }
197
mk_not_handled(TreeNode * f,char const * msg)198 void mk_not_handled(TreeNode* f, char const* msg) {
199 std::ostringstream strm;
200 strm << "Construct " << f->symbol() << " not handled: " << msg;
201 throw failure_ex(strm.str().c_str());
202 }
203
mk_input(TreeNode * f,named_formulas & fmls)204 void mk_input(TreeNode* f, named_formulas& fmls) {
205 if (!strcmp(f->symbol(),"annotated_formula")) {
206 mk_annotated_formula(f->child(0), fmls);
207 }
208 else if (!strcmp(f->symbol(),"include")) {
209 mk_include(f->child(2), f->child(3), fmls);
210 }
211 else {
212 mk_error(f, "annotated formula or include");
213 }
214 }
215
mk_annotated_formula(TreeNode * f,named_formulas & fmls)216 void mk_annotated_formula(TreeNode* f, named_formulas& fmls) {
217 if (!strcmp(f->symbol(),"fof_annotated")) {
218 fof_annotated(f->child(2), f->child(4), f->child(6), f->child(7), fmls);
219 }
220 else if (!strcmp(f->symbol(),"tff_annotated")) {
221 fof_annotated(f->child(2), f->child(4), f->child(6), f->child(7), fmls);
222 }
223 else if (!strcmp(f->symbol(),"cnf_annotated")) {
224 cnf_annotated(f->child(2), f->child(4), f->child(6), f->child(7), fmls);
225 }
226 else if (!strcmp(f->symbol(),"thf_annotated")) {
227 mk_error(f, "annotated formula (not thf)");
228 }
229 else {
230 mk_error(f, "annotated formula");
231 }
232 }
233
check_arity(unsigned num_args,unsigned arity)234 void check_arity(unsigned num_args, unsigned arity) {
235 if (num_args != arity) {
236 throw failure_ex("arity mismatch");
237 }
238 }
239
mk_include(TreeNode * file_name,TreeNode * formula_selection,named_formulas & fmls)240 void mk_include(TreeNode* file_name, TreeNode* formula_selection, named_formulas& fmls) {
241 char const* fn = file_name->child(0)->symbol();
242 TreeNode* name_list = formula_selection->child(2);
243 if (name_list && !strcmp("null",name_list->symbol())) {
244 name_list = 0;
245 }
246 std::string inc_name;
247 bool f_exists = false;
248 for (unsigned i = 1; !f_exists && i <= 3; ++i) {
249 inc_name.clear();
250 f_exists = mk_filename(fn, i, inc_name);
251
252 }
253 if (!f_exists) {
254 inc_name.clear();
255 f_exists = mk_env_filename(fn, inc_name);
256 }
257 if (!f_exists) {
258 inc_name = fn;
259 }
260
261 parse(inc_name.c_str(), fmls);
262 while (name_list) {
263 return mk_error(name_list, "name list (not handled)");
264 //char const* name = name_list->child(0)->symbol();
265 name_list = name_list->child(2);
266 }
267 }
268
269 #define CHECK(_node_) if (0 != strcmp(_node_->symbol(),#_node_)) return mk_error(_node_,#_node_);
270
get_name(TreeNode * name)271 const char* get_name(TreeNode* name) {
272 if (!name->child(0)) {
273 mk_error(name, "node with a child");
274 }
275 if (!name->child(0)->child(0)) {
276 return name->child(0)->symbol();
277 }
278 return name->child(0)->child(0)->symbol();
279 }
280
mk_forall(z3::expr_vector & bound,z3::expr body)281 z3::expr mk_forall(z3::expr_vector& bound, z3::expr body) {
282 return mk_quantifier(true, bound, body);
283 }
284
mk_quantifier(bool is_forall,z3::expr_vector & bound,z3::expr body)285 z3::expr mk_quantifier(bool is_forall, z3::expr_vector& bound, z3::expr body) {
286 Z3_app* vars = new Z3_app[bound.size()];
287 for (unsigned i = 0; i < bound.size(); ++i) {
288 vars[i] = (Z3_app) bound[i];
289 }
290 Z3_ast r = Z3_mk_quantifier_const(m_context, is_forall, 1, bound.size(), vars, 0, 0, body);
291 delete[] vars;
292 return z3::expr(m_context, r);
293 }
294
cnf_annotated(TreeNode * name,TreeNode * formula_role,TreeNode * formula,TreeNode * annotations,named_formulas & fmls)295 void cnf_annotated(TreeNode* name, TreeNode* formula_role, TreeNode* formula, TreeNode* annotations, named_formulas& fmls) {
296 symbol_set st;
297 get_cnf_variables(formula, st);
298 symbol_set::iterator it = st.begin(), end = st.end();
299 std::vector<z3::symbol> names;
300 m_bound.resize(0);
301 for(; it != end; ++it) {
302 names.push_back(*it);
303 m_bound.push_back(m_context.constant(names.back(), m_univ));
304 }
305 z3::expr r(m_context);
306 cnf_formula(formula, r);
307 if (!m_bound.empty()) {
308 r = mk_forall(m_bound, r);
309 }
310 char const* role = formula_role->child(0)->symbol();
311 if (!strcmp(role,"conjecture")) {
312 fmls.set_has_conjecture();
313 r = !r;
314 }
315 fmls.push_back(r, get_name(name), m_filename);
316 m_bound.resize(0);
317 }
318
cnf_formula(TreeNode * formula,z3::expr & r)319 void cnf_formula(TreeNode* formula, z3::expr& r) {
320 std::vector<z3::expr> disj;
321 if (formula->child(1)) {
322 disjunction(formula->child(1), disj);
323 }
324 else {
325 disjunction(formula->child(0), disj);
326 }
327 if (disj.size() > 0) {
328 r = disj[0];
329 }
330 else {
331 r = m_context.bool_val(false);
332 }
333 for (unsigned i = 1; i < disj.size(); ++i) {
334 r = r || disj[i];
335 }
336 }
337
disjunction(TreeNode * d,std::vector<z3::expr> & r)338 void disjunction(TreeNode* d, std::vector<z3::expr>& r) {
339 z3::expr lit(m_context);
340 if (d->child(2)) {
341 disjunction(d->child(0), r);
342 literal(d->child(2), lit);
343 r.push_back(lit);
344 }
345 else {
346 literal(d->child(0), lit);
347 r.push_back(lit);
348 }
349 }
350
literal(TreeNode * l,z3::expr & lit)351 void literal(TreeNode* l, z3::expr& lit) {
352 if (!strcmp(l->child(0)->symbol(),"~")) {
353 fof_formula(l->child(1), lit);
354 lit = !lit;
355 }
356 else {
357 fof_formula(l->child(0), lit);
358 }
359 }
360
fof_annotated(TreeNode * name,TreeNode * formula_role,TreeNode * formula,TreeNode * annotations,named_formulas & fmls)361 void fof_annotated(TreeNode* name, TreeNode* formula_role, TreeNode* formula, TreeNode* annotations, named_formulas& fmls) {
362 z3::expr fml(m_context);
363 //CHECK(fof_formula);
364 CHECK(formula_role);
365 fof_formula(formula->child(0), fml);
366 char const* role = formula_role->child(0)->symbol();
367 if (!strcmp(role,"conjecture")) {
368 fmls.set_has_conjecture();
369 fmls.push_back(!fml, get_name(name), m_filename);
370 }
371 else if (!strcmp(role,"type")) {
372 }
373 else {
374 fmls.push_back(fml, get_name(name), m_filename);
375 }
376 }
377
fof_formula(TreeNode * f,z3::expr & fml)378 void fof_formula(TreeNode* f, z3::expr& fml) {
379 z3::expr f1(m_context);
380 char const* name = f->symbol();
381 if (!strcmp(name,"fof_logic_formula") ||
382 !strcmp(name,"fof_binary_assoc") ||
383 !strcmp(name,"fof_binary_formula") ||
384 !strcmp(name,"tff_logic_formula") ||
385 !strcmp(name,"tff_binary_assoc") ||
386 !strcmp(name,"tff_binary_formula") ||
387 !strcmp(name,"atomic_formula") ||
388 !strcmp(name,"defined_atomic_formula")) {
389 fof_formula(f->child(0), fml);
390 }
391 else if (!strcmp(name, "fof_sequent") ||
392 !strcmp(name, "tff_sequent")) {
393 fof_formula(f->child(0), f1);
394 fof_formula(f->child(2), fml);
395 fml = implies(f1, fml);
396 }
397 else if (!strcmp(name, "fof_binary_nonassoc") ||
398 !strcmp(name, "tff_binary_nonassoc")) {
399 fof_formula(f->child(0), f1);
400 fof_formula(f->child(2), fml);
401 //SASSERT(!strcmp("binary_connective",f->child(1)->symbol()));
402 char const* conn = f->child(1)->child(0)->symbol();
403 if (!strcmp(conn, "<=>")) {
404 fml = (f1 == fml);
405 }
406 else if (!strcmp(conn, "=>")) {
407 fml = implies(f1, fml);
408 }
409 else if (!strcmp(conn, "<=")) {
410 fml = implies(fml, f1);
411 }
412 else if (!strcmp(conn, "<~>")) {
413 fml = ! (f1 == fml);
414 }
415 else if (!strcmp(conn, "~|")) {
416 fml = !(f1 || fml);
417 }
418 else if (!strcmp(conn, "~&")) {
419 fml = ! (f1 && fml);
420 }
421 else {
422 mk_error(f->child(1)->child(0), "connective");
423 }
424 }
425 else if (!strcmp(name,"fof_or_formula") ||
426 !strcmp(name,"tff_or_formula")) {
427 fof_formula(f->child(0), f1);
428 fof_formula(f->child(2), fml);
429 fml = f1 || fml;
430 }
431 else if (!strcmp(name,"fof_and_formula") ||
432 !strcmp(name,"tff_and_formula")) {
433 fof_formula(f->child(0), f1);
434 fof_formula(f->child(2), fml);
435 fml = f1 && fml;
436 }
437 else if (!strcmp(name,"fof_unitary_formula") ||
438 !strcmp(name,"tff_unitary_formula")) {
439 if (f->child(1)) {
440 // parenthesis
441 fof_formula(f->child(1), fml);
442 }
443 else {
444 fof_formula(f->child(0), fml);
445 }
446 }
447 else if (!strcmp(name,"fof_quantified_formula") ||
448 !strcmp(name,"tff_quantified_formula")) {
449 fof_quantified_formula(f->child(0), f->child(2), f->child(5), fml);
450 }
451 else if (!strcmp(name,"fof_unary_formula") ||
452 !strcmp(name,"tff_unary_formula")) {
453 if (!f->child(1)) {
454 fof_formula(f->child(0), fml);
455 }
456 else {
457 fof_formula(f->child(1), fml);
458 char const* conn = f->child(0)->child(0)->symbol();
459 if (!strcmp(conn,"~")) {
460 fml = !fml;
461 }
462 else {
463 mk_error(f->child(0)->child(0), "fof_unary_formula");
464 }
465 }
466 }
467 else if (!strcmp(name,"fof_let")) {
468 mk_let(f->child(2), f->child(5), fml);
469 }
470 else if (!strcmp(name,"variable")) {
471 char const* v = f->child(0)->symbol();
472 if (!find_bound(v, fml)) {
473 mk_error(f->child(0), "variable");
474 }
475 }
476 else if (!strcmp(name,"fof_conditional")) {
477 z3::expr f2(m_context);
478 fof_formula(f->child(2), f1);
479 fof_formula(f->child(4), f2);
480 fof_formula(f->child(6), fml);
481 fml = ite(f1, f2, fml);
482 }
483 else if (!strcmp(name,"plain_atomic_formula") ||
484 !strcmp(name,"defined_plain_formula") ||
485 !strcmp(name,"system_atomic_formula")) {
486 z3::sort srt(m_context.bool_sort());
487 term(f->child(0), srt, fml);
488 }
489 else if (!strcmp(name,"defined_infix_formula") ||
490 !strcmp(name,"fol_infix_unary")) {
491 z3::expr t1(m_context), t2(m_context);
492 term(f->child(0), m_univ, t1);
493 term(f->child(2), m_univ, t2);
494 TreeNode* inf = f->child(1);
495 while (inf && strcmp(inf->symbol(),"=") && strcmp(inf->symbol(),"!=")) {
496 inf = inf->child(0);
497 }
498 if (!inf) {
499 mk_error(f->child(1), "defined_infix_formula");
500 }
501 char const* conn = inf->symbol();
502 if (!strcmp(conn,"=")) {
503 fml = t1 == t2;
504 }
505 else if (!strcmp(conn,"!=")) {
506 fml = ! (t1 == t2);
507 }
508 else {
509 mk_error(inf, "defined_infix_formula");
510 }
511 }
512 else if (!strcmp(name, "tff_typed_atom")) {
513 while (!strcmp(f->child(0)->symbol(),"(")) {
514 f = f->child(1);
515 }
516 char const* id = 0;
517 z3::sort s(m_context);
518 z3::sort_vector sorts(m_context);
519
520 mk_id(f->child(0), id);
521 if (is_ttype(f->child(2))) {
522 s = mk_sort(id);
523 m_defined_sorts.insert(symbol(id), s);
524 }
525 else {
526 mk_mapping_sort(f->child(2), sorts, s);
527 z3::func_decl fd(m_context.function(id, sorts, s));
528 m_decls.insert(symbol(id), fd);
529 }
530 }
531 else {
532 mk_error(f, "fof_formula");
533 }
534 }
535
is_ttype(TreeNode * t)536 bool is_ttype(TreeNode* t) {
537 char const* name = t->symbol();
538 if (!strcmp(name,"atomic_defined_word")) {
539 return !strcmp("$tType", t->child(0)->symbol());
540 }
541 return false;
542 }
543
fof_quantified_formula(TreeNode * fol_quantifier,TreeNode * vl,TreeNode * formula,z3::expr & fml)544 void fof_quantified_formula(TreeNode* fol_quantifier, TreeNode* vl, TreeNode* formula, z3::expr& fml) {
545 unsigned l = m_bound.size();
546 mk_variable_list(vl);
547 fof_formula(formula, fml);
548 bool is_forall = !strcmp(fol_quantifier->child(0)->symbol(),"!");
549 z3::expr_vector bound(m_context);
550 for (unsigned i = l; i < m_bound.size(); ++i) {
551 bound.push_back(m_bound[i]);
552 }
553 fml = mk_quantifier(is_forall, bound, fml);
554 m_bound.resize(l);
555 }
556
mk_variable_list(TreeNode * variable_list)557 void mk_variable_list(TreeNode* variable_list) {
558 while (variable_list) {
559 TreeNode* var = variable_list->child(0);
560 if (!strcmp(var->symbol(),"tff_variable")) {
561 var = var->child(0);
562 }
563 if (!strcmp(var->symbol(),"variable")) {
564 char const* name = var->child(0)->symbol();
565 m_bound.push_back(m_context.constant(name, m_univ));
566 }
567 else if (!strcmp(var->symbol(),"tff_typed_variable")) {
568 z3::sort s(m_context);
569 char const* name = var->child(0)->child(0)->symbol();
570 mk_sort(var->child(2), s);
571 m_bound.push_back(m_context.constant(name, s));
572 }
573 else {
574 mk_error(var, "variable_list");
575 }
576 variable_list = variable_list->child(2);
577 }
578 }
579
mk_sort(TreeNode * t,z3::sort & s)580 void mk_sort(TreeNode* t, z3::sort& s) {
581 char const* name = t->symbol();
582 if (!strcmp(name, "tff_atomic_type") ||
583 !strcmp(name, "defined_type")) {
584 mk_sort(t->child(0), s);
585 }
586 else if (!strcmp(name, "atomic_defined_word")) {
587 z3::symbol sname = symbol(t->child(0)->symbol());
588 z3::sort srt(m_context);
589 if (!strcmp("$tType", t->child(0)->symbol())) {
590 char const* id = 0;
591 s = mk_sort(id);
592 m_defined_sorts.insert(symbol(id), s);
593 }
594 else if (m_defined_sorts.find(sname, srt)) {
595 s = srt;
596 }
597 else {
598 s = mk_sort(sname);
599 if (sname == symbol("$rat")) {
600 throw failure_ex("rational sorts are not handled\n");
601 }
602 mk_error(t, sname.str().c_str());
603 }
604 }
605 else if (!strcmp(name,"atomic_word")) {
606 name = t->child(0)->symbol();
607 z3::symbol symname = symbol(name);
608 s = mk_sort(symname);
609 }
610 else {
611 mk_error(t, "sort");
612 }
613 }
614
mk_mapping_sort(TreeNode * t,z3::sort_vector & domain,z3::sort & s)615 void mk_mapping_sort(TreeNode* t, z3::sort_vector& domain, z3::sort& s) {
616 char const* name = t->symbol();
617 //char const* id = 0;
618 if (!strcmp(name,"tff_top_level_type")) {
619 mk_mapping_sort(t->child(0), domain, s);
620 }
621 else if (!strcmp(name,"tff_atomic_type")) {
622 mk_sort(t->child(0), s);
623 }
624 else if (!strcmp(name,"tff_mapping_type")) {
625 TreeNode* t1 = t->child(0);
626 if (t1->child(1)) {
627 mk_xprod_sort(t1->child(1), domain);
628 }
629 else {
630 mk_sort(t1->child(0), s);
631 domain.push_back(s);
632 }
633 mk_sort(t->child(2), s);
634 }
635 else {
636 mk_error(t, "mapping sort");
637 }
638 }
639
mk_xprod_sort(TreeNode * t,z3::sort_vector & sorts)640 void mk_xprod_sort(TreeNode* t, z3::sort_vector& sorts) {
641 char const* name = t->symbol();
642 z3::sort s1(m_context), s2(m_context);
643 if (!strcmp(name, "tff_atomic_type")) {
644 mk_sort(t->child(0), s1);
645 sorts.push_back(s1);
646 }
647 else if (!strcmp(name, "tff_xprod_type")) {
648 name = t->child(0)->symbol();
649 if (!strcmp(name, "tff_atomic_type") ||
650 !strcmp(name, "tff_xprod_type")) {
651 mk_xprod_sort(t->child(0), sorts);
652 mk_xprod_sort(t->child(2), sorts);
653 }
654 else if (t->child(1)) {
655 mk_xprod_sort(t->child(1), sorts);
656 }
657 else {
658 mk_error(t, "xprod sort");
659 }
660 }
661 else {
662 mk_error(t, "xprod sort");
663 }
664 }
665
term(TreeNode * t,z3::sort const & s,z3::expr & r)666 void term(TreeNode* t, z3::sort const& s, z3::expr& r) {
667 char const* name = t->symbol();
668 if (!strcmp(name, "defined_plain_term") ||
669 !strcmp(name, "system_term") ||
670 !strcmp(name, "plain_term")) {
671 if (!t->child(1)) {
672 term(t->child(0), s, r);
673 }
674 else {
675 apply_term(t->child(0), t->child(2), s, r);
676 }
677 }
678 else if (!strcmp(name, "constant") ||
679 !strcmp(name, "functor") ||
680 !strcmp(name, "defined_plain_formula") ||
681 !strcmp(name, "defined_functor") ||
682 !strcmp(name, "defined_constant") ||
683 !strcmp(name, "system_constant") ||
684 !strcmp(name, "defined_atomic_term") ||
685 !strcmp(name, "system_functor") ||
686 !strcmp(name, "function_term") ||
687 !strcmp(name, "term") ||
688 !strcmp(name, "defined_term")) {
689 term(t->child(0), s, r);
690 }
691
692
693 else if (!strcmp(name, "defined_atom")) {
694 char const* name0 = t->child(0)->symbol();
695 if (!strcmp(name0,"number")) {
696 name0 = t->child(0)->child(0)->symbol();
697 char const* per = strchr(name0, '.');
698 bool is_real = 0 != per;
699 bool is_rat = 0 != strchr(name0, '/');
700 bool is_int = !is_real && !is_rat;
701 if (is_int) {
702 r = m_context.int_val(name0);
703 }
704 else {
705 r = m_context.real_val(name0);
706 }
707 }
708 else if (!strcmp(name0, "distinct_object")) {
709 throw failure_ex("distinct object not handled");
710 }
711 else {
712 mk_error(t->child(0), "number or distinct object");
713 }
714 }
715 else if (!strcmp(name, "atomic_defined_word")) {
716 char const* ch = t->child(0)->symbol();
717 z3::symbol s = symbol(ch);
718 z3::func_decl fd(m_context);
719 if (!strcmp(ch, "$true")) {
720 r = m_context.bool_val(true);
721 }
722 else if (!strcmp(ch, "$false")) {
723 r = m_context.bool_val(false);
724 }
725 else if (m_decls.find(s, fd)) {
726 r = fd(0,0);
727 }
728 else {
729 mk_error(t->child(0), "atomic_defined_word");
730 }
731 }
732 else if (!strcmp(name, "atomic_word")) {
733 z3::func_decl f(m_context);
734 z3::symbol sym = symbol(t->child(0)->symbol());
735 if (m_decls.find(sym, f)) {
736 r = f(0,0);
737 }
738 else {
739 r = m_context.constant(sym, s);
740 }
741 }
742 else if (!strcmp(name, "variable")) {
743 char const* v = t->child(0)->symbol();
744 if (!find_bound(v, r)) {
745 mk_error(t->child(0), "variable not bound");
746 }
747 }
748 else {
749 mk_error(t, "term not recognized");
750 }
751 }
752
apply_term(TreeNode * f,TreeNode * args,z3::sort const & s,z3::expr & r)753 void apply_term(TreeNode* f, TreeNode* args, z3::sort const& s, z3::expr& r) {
754 z3::expr_vector terms(m_context);
755 z3::sort_vector sorts(m_context);
756 mk_args(args, terms);
757 for (unsigned i = 0; i < terms.size(); ++i) {
758 sorts.push_back(terms[i].get_sort());
759 }
760 if (!strcmp(f->symbol(),"functor") ||
761 !strcmp(f->symbol(),"system_functor") ||
762 !strcmp(f->symbol(),"defined_functor")) {
763 f = f->child(0);
764 }
765 bool atomic_word = !strcmp(f->symbol(),"atomic_word");
766 if (atomic_word ||
767 !strcmp(f->symbol(),"atomic_defined_word") ||
768 !strcmp(f->symbol(),"atomic_system_word")) {
769 char const* ch = f->child(0)->symbol();
770 z3::symbol fn = symbol(ch);
771 z3::func_decl fun(m_context);
772 z3::context& ctx = r.ctx();
773 if (!strcmp(ch,"$less")) {
774 check_arity(terms.size(), 2);
775 r = terms[0] < terms[1];
776 }
777 else if (!strcmp(ch,"$lesseq")) {
778 check_arity(terms.size(), 2);
779 r = terms[0] <= terms[1];
780 }
781 else if (!strcmp(ch,"$greater")) {
782 check_arity(terms.size(), 2);
783 r = terms[0] > terms[1];
784 }
785 else if (!strcmp(ch,"$greatereq")) {
786 check_arity(terms.size(), 2);
787 r = terms[0] >= terms[1];
788 }
789 else if (!strcmp(ch,"$uminus")) {
790 check_arity(terms.size(), 1);
791 r = -terms[0];
792 }
793 else if (!strcmp(ch,"$sum")) {
794 check_arity(terms.size(), 2);
795 r = terms[0] + terms[1];
796 }
797 else if (!strcmp(ch,"$plus")) {
798 check_arity(terms.size(), 2);
799 r = terms[0] + terms[1];
800 }
801 else if (!strcmp(ch,"$difference")) {
802 check_arity(terms.size(), 2);
803 r = terms[0] - terms[1];
804 }
805 else if (!strcmp(ch,"$product")) {
806 check_arity(terms.size(), 2);
807 r = terms[0] * terms[1];
808 }
809 else if (!strcmp(ch,"$quotient")) {
810 check_arity(terms.size(), 2);
811 r = terms[0] / terms[1];
812 }
813 else if (!strcmp(ch,"$quotient_e")) {
814 check_arity(terms.size(), 2);
815 r = terms[0] / terms[1];
816 }
817 else if (!strcmp(ch,"$distinct")) {
818 if (terms.size() == 2) {
819 r = terms[0] != terms[1];
820 }
821 else {
822 r = distinct(terms);
823 }
824 }
825 else if (!strcmp(ch,"$floor") || !strcmp(ch,"$to_int")) {
826 check_arity(terms.size(), 1);
827 r = to_real(to_int(terms[0]));
828 }
829 else if (!strcmp(ch,"$to_real")) {
830 check_arity(terms.size(), 1);
831 r = terms[0];
832 if (r.get_sort().is_int()) {
833 r = to_real(terms[0]);
834 }
835 }
836 else if (!strcmp(ch,"$is_int")) {
837 check_arity(terms.size(), 1);
838 r = z3::expr(ctx, Z3_mk_is_int(ctx, terms[0]));
839 }
840 else if (!strcmp(ch,"$true")) {
841 r = ctx.bool_val(true);
842 }
843 else if (!strcmp(ch,"$false")) {
844 r = ctx.bool_val(false);
845 }
846 // ceiling(x) = -floor(-x)
847 else if (!strcmp(ch,"$ceiling")) {
848 check_arity(terms.size(), 1);
849 r = ceiling(terms[0]);
850 }
851 // truncate - The nearest integral value with magnitude not greater than the absolute value of the argument.
852 // if x >= 0 floor(x) else ceiling(x)
853 else if (!strcmp(ch,"$truncate")) {
854 check_arity(terms.size(), 1);
855 r = truncate(terms[0]);
856 }
857 // The nearest integral number to the argument. When the argument
858 // is halfway between two integral numbers, the nearest even integral number to the argument.
859 else if (!strcmp(ch,"$round")) {
860 check_arity(terms.size(), 1);
861 z3::expr t = terms[0];
862 z3::expr i = to_int(t);
863 z3::expr i2 = i + ctx.real_val(1,2);
864 r = ite(t > i2, i + 1, ite(t == i2, ite(is_even(i), i, i+1), i));
865 }
866 // $quotient_e(N,D) - the Euclidean quotient, which has a non-negative remainder.
867 // If D is positive then $quotient_e(N,D) is the floor (in the type of N and D) of
868 // the real division N/D, and if D is negative then $quotient_e(N,D) is the ceiling of N/D.
869
870 // $quotient_t(N,D) - the truncation of the real division N/D.
871 else if (!strcmp(ch,"$quotient_t")) {
872 check_arity(terms.size(), 2);
873 r = truncate(terms[0] / terms[1]);
874 }
875 // $quotient_f(N,D) - the floor of the real division N/D.
876 else if (!strcmp(ch,"$quotient_f")) {
877 check_arity(terms.size(), 2);
878 r = to_real(to_int(terms[0] / terms[1]));
879 }
880 // For t in {$int,$rat, $real}, x in {e, t,f}, $quotient_x and $remainder_x are related by
881 // ! [N:t,D:t] : $sum($product($quotient_x(N,D),D),$remainder_x(N,D)) = N
882 // For zero divisors the result is not specified.
883 else if (!strcmp(ch,"$remainder_t")) {
884 mk_not_handled(f, ch);
885 }
886 else if (!strcmp(ch,"$remainder_e")) {
887 check_arity(terms.size(), 2);
888 r = z3::expr(ctx, Z3_mk_mod(ctx, terms[0], terms[1]));
889 }
890 else if (!strcmp(ch,"$remainder_r")) {
891 mk_not_handled(f, ch);
892 }
893 else if (!strcmp(ch,"$to_rat") ||
894 !strcmp(ch,"$is_rat")) {
895 mk_not_handled(f, ch);
896 }
897 else if (m_decls.find(fn, fun)) {
898 r = fun(terms);
899 }
900 else if (true) {
901 z3::func_decl func(m_context);
902 func = m_context.function(fn, sorts, s);
903 r = func(terms);
904 }
905 else {
906 mk_error(f->child(0), "atomic, defined or system word");
907 }
908 return;
909 }
910 mk_error(f, "function");
911 }
912
to_int(z3::expr e)913 z3::expr to_int(z3::expr e) {
914 return z3::expr(e.ctx(), Z3_mk_real2int(e.ctx(), e));
915 }
916
to_real(z3::expr e)917 z3::expr to_real(z3::expr e) {
918 return z3::expr(e.ctx(), Z3_mk_int2real(e.ctx(), e));
919 }
920
ceiling(z3::expr e)921 z3::expr ceiling(z3::expr e) {
922 return -to_real(to_int(-e));
923 }
924
is_even(z3::expr e)925 z3::expr is_even(z3::expr e) {
926 z3::context& ctx = e.ctx();
927 z3::expr two = ctx.int_val(2);
928 z3::expr m = z3::expr(ctx, Z3_mk_mod(ctx, e, two));
929 return m == 0;
930 }
931
truncate(z3::expr e)932 z3::expr truncate(z3::expr e) {
933 return ite(e >= 0, to_int(e), ceiling(e));
934 }
935
check_app(z3::func_decl & f,unsigned num,z3::expr const * args)936 bool check_app(z3::func_decl& f, unsigned num, z3::expr const* args) {
937 if (f.arity() == num) {
938 for (unsigned i = 0; i < num; ++i) {
939 if (!eq(args[i].get_sort(), f.domain(i))) {
940 return false;
941 }
942 }
943 return true;
944 }
945 else {
946 return true;
947 }
948 }
949
mk_args(TreeNode * args,z3::expr_vector & result)950 void mk_args(TreeNode* args, z3::expr_vector& result) {
951 z3::expr t(m_context);
952 while (args) {
953 term(args->child(0), m_univ, t);
954 result.push_back(t);
955 args = args->child(2);
956 }
957 }
958
959
find_bound(char const * v,z3::expr & b)960 bool find_bound(char const* v, z3::expr& b) {
961 for (unsigned l = m_bound.size(); l > 0; ) {
962 --l;
963 if (v == m_bound[l].decl().name().str()) {
964 b = m_bound[l];
965 return true;
966 }
967 }
968 return false;
969 }
970
mk_id(TreeNode * f,char const * & sym)971 void mk_id(TreeNode* f, char const*& sym) {
972 char const* name = f->symbol();
973 if (!strcmp(name, "tff_untyped_atom") ||
974 !strcmp(name, "functor") ||
975 !strcmp(name, "system_functor")) {
976 mk_id(f->child(0), sym);
977 }
978 else if (!strcmp(name, "atomic_word") ||
979 !strcmp(name, "atomic_system_word")) {
980 sym = f->child(0)->symbol();
981 }
982 else {
983 mk_error(f, "atom");
984 }
985 }
986
mk_let(TreeNode * let_vars,TreeNode * f,z3::expr & fml)987 void mk_let(TreeNode* let_vars, TreeNode* f, z3::expr& fml) {
988 mk_error(f, "let construct is not handled");
989 }
990
open_file(char const * filename)991 FILE* open_file(char const* filename) {
992 FILE* fp = 0;
993 #ifdef _WINDOWS
994 if (0 > fopen_s(&fp, filename, "r") || fp == 0) {
995 fp = 0;
996 }
997 #else
998 fp = fopen(filename, "r");
999 #endif
1000 return fp;
1001 }
1002
is_sep(char s)1003 bool is_sep(char s) {
1004 return s == '/' || s == '\\';
1005 }
1006
add_separator(const char * rel_name,std::string & inc_name)1007 void add_separator(const char* rel_name, std::string& inc_name) {
1008 size_t sz = inc_name.size();
1009 if (sz == 0) return;
1010 if (sz > 0 && is_sep(inc_name[sz-1])) return;
1011 if (is_sep(rel_name[0])) return;
1012 inc_name += "/";
1013 }
1014
append_rel_name(const char * rel_name,std::string & inc_name)1015 void append_rel_name(const char * rel_name, std::string& inc_name) {
1016 if (rel_name[0] == '\'') {
1017 add_separator(rel_name+1, inc_name);
1018 inc_name.append(rel_name+1);
1019 inc_name.resize(inc_name.size()-1);
1020 }
1021 else {
1022 add_separator(rel_name, inc_name);
1023 inc_name.append(rel_name);
1024 }
1025 }
1026
mk_filename(const char * rel_name,unsigned num_sep,std::string & inc_name)1027 bool mk_filename(const char *rel_name, unsigned num_sep, std::string& inc_name) {
1028 unsigned sep1 = 0, sep2 = 0, sep3 = 0;
1029 size_t len = strlen(m_filename);
1030 for (unsigned i = 0; i < len; ++i) {
1031 if (is_sep(m_filename[i])) {
1032 sep3 = sep2;
1033 sep2 = sep1;
1034 sep1 = i;
1035 }
1036 }
1037 if ((num_sep == 3) && sep3 > 0) {
1038 inc_name.append(m_filename,sep3+1);
1039 }
1040 if ((num_sep == 2) && sep2 > 0) {
1041 inc_name.append(m_filename,sep2+1);
1042 }
1043 if ((num_sep == 1) && sep1 > 0) {
1044 inc_name.append(m_filename,sep1+1);
1045 }
1046 append_rel_name(rel_name, inc_name);
1047 return file_exists(inc_name.c_str());
1048 }
1049
file_exists(char const * filename)1050 bool file_exists(char const* filename) {
1051 FILE* fp = open_file(filename);
1052 if (!fp) {
1053 return false;
1054 }
1055 fclose(fp);
1056 return true;
1057 }
1058
mk_env_filename(const char * rel_name,std::string & inc_name)1059 bool mk_env_filename(const char* rel_name, std::string& inc_name) {
1060 #ifdef _WINDOWS
1061 char buffer[1024];
1062 size_t sz;
1063 errno_t err = getenv_s(
1064 &sz,
1065 buffer,
1066 "$TPTP");
1067 if (err != 0) {
1068 return false;
1069 }
1070 #else
1071 char const* buffer = getenv("$TPTP");
1072 if (!buffer) {
1073 return false;
1074 }
1075 #endif
1076 inc_name = buffer;
1077 append_rel_name(rel_name, inc_name);
1078 return file_exists(inc_name.c_str());
1079 }
1080
get_cnf_variables(TreeNode * t,symbol_set & symbols)1081 void get_cnf_variables(TreeNode* t, symbol_set& symbols) {
1082 std::vector<TreeNode*> todo;
1083 todo.push_back(t);
1084 while (!todo.empty()) {
1085 t = todo.back();
1086 todo.pop_back();
1087 if (!t) continue;
1088 if (!strcmp(t->symbol(),"variable")) {
1089 z3::symbol sym = symbol(t->child(0)->symbol());
1090 symbols.insert(sym);
1091 }
1092 else {
1093 for (unsigned i = 0; i < 10; ++i) {
1094 todo.push_back(t->child(i));
1095 }
1096 }
1097 }
1098 }
1099
symbol(char const * s)1100 z3::symbol symbol(char const* s) {
1101 return m_context.str_symbol(s);
1102 }
1103
mk_sort(char const * s)1104 z3::sort mk_sort(char const* s) {
1105 return m_context.uninterpreted_sort(s);
1106 }
1107
mk_sort(z3::symbol & s)1108 z3::sort mk_sort(z3::symbol& s) {
1109 return m_context.uninterpreted_sort(s);
1110 }
1111
1112 public:
env(z3::context & ctx)1113 env(z3::context& ctx):
1114 m_context(ctx),
1115 m_bound(ctx),
1116 m_univ(mk_sort("$i")),
1117 m_filename(0) {
1118 m_nodes = 0;
1119 m_region = new alloc_region();
1120 m_defined_sorts.insert(symbol("$i"), m_univ);
1121 m_defined_sorts.insert(symbol("$o"), m_context.bool_sort());
1122 m_defined_sorts.insert(symbol("$real"), m_context.real_sort());
1123 m_defined_sorts.insert(symbol("$int"), m_context.int_sort());
1124
1125 }
1126
~env()1127 ~env() {
1128 delete m_region;
1129 m_region = 0;
1130 }
1131 void parse(const char* filename, named_formulas& fmls);
register_node(TreeNode * t)1132 static void register_node(TreeNode* t) { m_nodes->push_back(t); }
r()1133 static alloc_region& r() { return *m_region; }
1134 };
1135
1136 std::vector<TreeNode*>* env::m_nodes = 0;
1137 alloc_region* env::m_region = 0;
1138
1139 # define P_USERPROC
1140 # define P_ACT(ss) if(verbose)printf("%7d %s\n",yylineno,ss);
1141 # define P_BUILD(sym,A,B,C,D,E,F,G,H,I,J) new (env::r()) TreeNode(env::r(), sym,A,B,C,D,E,F,G,H,I,J)
1142 # define P_TOKEN(tok,symbolIndex) MkToken(env::r(), tok,symbolIndex)
1143 # define P_PRINT(ss) env::register_node(ss)
1144
1145
1146 // ------------------------------------------------------
1147 // created by YACC.
1148 #include "tptp5.tab.c"
1149
1150 extern FILE* yyin;
1151
1152
parse(const char * filename,named_formulas & fmls)1153 void env::parse(const char* filename, named_formulas& fmls) {
1154 std::vector<TreeNode*> nodes;
1155 flet<char const*> fn(m_filename, filename);
1156 flet<std::vector<TreeNode*>*> fnds(m_nodes, &nodes);
1157
1158 FILE* fp = open_file(filename);
1159 if (!fp) {
1160 std::stringstream strm;
1161 strm << "Could not open file " << filename << "\n";
1162 throw failure_ex(strm.str().c_str());
1163 }
1164 yyin = fp;
1165 int result = yyparse();
1166 fclose(fp);
1167
1168 if (result != 0) {
1169 throw failure_ex("could not parse input");
1170 }
1171
1172 for (unsigned i = 0; i < nodes.size(); ++i) {
1173 TreeNode* cl = nodes[i];
1174 if (cl) {
1175 mk_input(cl, fmls);
1176 }
1177 }
1178
1179 }
1180
1181 class pp_tptp {
1182 z3::context& ctx;
1183 std::vector<std::string> names;
1184 std::vector<z3::sort> sorts;
1185 std::vector<z3::func_decl> funs;
1186 std::vector<z3::expr> todo;
1187 std::set<unsigned> seen_ids;
1188 unsigned m_formula_id;
1189 unsigned m_node_number;
1190 std::map<unsigned, unsigned> m_proof_ids;
1191 std::map<unsigned, std::set<unsigned> > m_proof_hypotheses;
1192 std::map<unsigned, unsigned> m_axiom_ids;
1193 named_formulas* m_named_formulas;
1194
1195 public:
pp_tptp(z3::context & ctx)1196 pp_tptp(z3::context& ctx): ctx(ctx), m_formula_id(0) {}
1197
1198
display_func_decl(std::ostream & out,z3::func_decl & f)1199 void display_func_decl(std::ostream& out, z3::func_decl& f) {
1200 std::string name = lower_case_fun(f.name());
1201 out << "tff(" << name << "_type, type, (\n " << name << ": ";
1202 unsigned na = f.arity();
1203 switch(na) {
1204 case 0:
1205 break;
1206 case 1: {
1207 z3::sort s(f.domain(0));
1208 display_sort(out, s);
1209 out << " > ";
1210 break;
1211 }
1212 default:
1213 out << "( ";
1214 for (unsigned j = 0; j < na; ++j) {
1215 z3::sort s(f.domain(j));
1216 display_sort(out, s);
1217 if (j + 1 < na) {
1218 out << " * ";
1219 }
1220 }
1221 out << " ) > ";
1222 }
1223 z3::sort srt(f.range());
1224 display_sort(out, srt);
1225 out << ")).\n";
1226 }
1227
display_axiom(std::ostream & out,z3::expr e)1228 void display_axiom(std::ostream& out, z3::expr e) {
1229 out << "tff(formula" << (++m_formula_id) << ", axiom,\n ";
1230 display(out, e, true);
1231 out << ").\n";
1232 }
1233
display(std::ostream & out,z3::expr e,bool in_paren)1234 void display(std::ostream& out, z3::expr e, bool in_paren) {
1235 std::string s;
1236 if (e.is_numeral(s)) {
1237 out << s;
1238 }
1239 else if (e.is_var()) {
1240 unsigned idx = Z3_get_index_value(ctx, e);
1241 out << names[names.size()-1-idx];
1242 }
1243 else if (e.is_app()) {
1244 switch(e.decl().decl_kind()) {
1245 case Z3_OP_TRUE:
1246 out << "$true";
1247 break;
1248 case Z3_OP_FALSE:
1249 out << "$false";
1250 break;
1251 case Z3_OP_AND:
1252 display_infix(out, "&", e, in_paren);
1253 break;
1254 case Z3_OP_OR:
1255 display_infix(out, "|", e, in_paren);
1256 break;
1257 case Z3_OP_IMPLIES:
1258 display_infix(out, "=>", e, in_paren);
1259 break;
1260 case Z3_OP_NOT:
1261 if (!in_paren) out << "(";
1262 out << "~";
1263 display(out, e.arg(0), false);
1264 if (!in_paren) out << ")";
1265 break;
1266 case Z3_OP_EQ:
1267 if (e.arg(0).is_bool()) {
1268 display_infix(out, "<=>", e, in_paren);
1269 }
1270 else {
1271 display_infix(out, "=", e, in_paren);
1272 }
1273 break;
1274 case Z3_OP_IFF:
1275 display_infix(out, "<=>", e, in_paren);
1276 break;
1277 case Z3_OP_XOR:
1278 display_infix(out, "<~>", e, in_paren);
1279 break;
1280 case Z3_OP_MUL:
1281 display_binary(out, "$product", e);
1282 break;
1283 case Z3_OP_ADD:
1284 display_binary(out, "$sum", e);
1285 break;
1286 case Z3_OP_SUB:
1287 display_prefix(out, "$difference", e);
1288 break;
1289 case Z3_OP_LE:
1290 display_prefix(out, "$lesseq", e);
1291 break;
1292 case Z3_OP_GE:
1293 display_prefix(out, "$greatereq", e);
1294 break;
1295 case Z3_OP_LT:
1296 display_prefix(out, "$less", e);
1297 break;
1298 case Z3_OP_GT:
1299 display_prefix(out, "$greater", e);
1300 break;
1301 case Z3_OP_UMINUS:
1302 display_prefix(out, "$uminus", e);
1303 break;
1304 case Z3_OP_DIV:
1305 display_prefix(out, "$quotient", e);
1306 break;
1307 case Z3_OP_IS_INT:
1308 display_prefix(out, "$is_int", e);
1309 break;
1310 case Z3_OP_TO_REAL:
1311 display_prefix(out, "$to_real", e);
1312 break;
1313 case Z3_OP_TO_INT:
1314 display_prefix(out, "$to_int", e);
1315 break;
1316 case Z3_OP_IDIV:
1317 display_prefix(out, "$quotient_e", e);
1318 break;
1319 case Z3_OP_MOD:
1320 display_prefix(out, "$remainder_e", e);
1321 break;
1322 case Z3_OP_ITE:
1323 display_prefix(out, e.is_bool()?"ite_f":"ite_t", e);
1324 break;
1325 case Z3_OP_DISTINCT:
1326 display_prefix(out, "$distinct", e);
1327 break;
1328 case Z3_OP_REM:
1329 throw failure_ex("rem is not handled");
1330 break;
1331 case Z3_OP_OEQ:
1332 display_prefix(out, "$oeq", e);
1333 break;
1334 default:
1335 display_app(out, e);
1336 break;
1337 }
1338 }
1339 else if (e.is_quantifier()) {
1340 bool is_forall = Z3_is_quantifier_forall(ctx, e);
1341 bool is_lambda = Z3_is_lambda(ctx, e);
1342 unsigned nb = Z3_get_quantifier_num_bound(ctx, e);
1343
1344 out << (is_lambda?"^":(is_forall?"!":"?")) << "[";
1345 for (unsigned i = 0; i < nb; ++i) {
1346 Z3_symbol n = Z3_get_quantifier_bound_name(ctx, e, i);
1347 names.push_back(upper_case_var(z3::symbol(ctx, n)));
1348 z3::sort srt(ctx, Z3_get_quantifier_bound_sort(ctx, e, i));
1349 out << names.back() << ": ";
1350 display_sort(out, srt);
1351 if (i + 1 < nb) {
1352 out << ", ";
1353 }
1354 }
1355 out << "] : ";
1356 display(out, e.body(), false);
1357 for (unsigned i = 0; i < nb; ++i) {
1358 names.pop_back();
1359 }
1360 }
1361 }
1362
display_app(std::ostream & out,z3::expr e)1363 void display_app(std::ostream& out, z3::expr e) {
1364 if (e.is_const()) {
1365 out << e;
1366 return;
1367 }
1368 out << lower_case_fun(e.decl().name()) << "(";
1369 unsigned n = e.num_args();
1370 for(unsigned i = 0; i < n; ++i) {
1371 display(out, e.arg(i), n == 1);
1372 if (i + 1 < n) {
1373 out << ", ";
1374 }
1375 }
1376 out << ")";
1377 }
1378
display_sort(std::ostream & out,z3::sort const & s)1379 void display_sort(std::ostream& out, z3::sort const& s) {
1380 if (s.is_int()) {
1381 out << "$int";
1382 }
1383 else if (s.is_real()) {
1384 out << "$real";
1385 }
1386 else if (s.is_bool()) {
1387 out << "$o";
1388 }
1389 else {
1390 out << s;
1391 }
1392 }
1393
display_infix(std::ostream & out,char const * conn,z3::expr & e,bool in_paren)1394 void display_infix(std::ostream& out, char const* conn, z3::expr& e, bool in_paren) {
1395 if (!in_paren) out << "(";
1396 unsigned sz = e.num_args();
1397 for (unsigned i = 0; i < sz; ++i) {
1398 display(out, e.arg(i), false);
1399 if (i + 1 < sz) {
1400 out << " " << conn << " ";
1401 }
1402 }
1403 if (!in_paren) out << ")";
1404 }
1405
display_prefix(std::ostream & out,char const * conn,z3::expr & e)1406 void display_prefix(std::ostream& out, char const* conn, z3::expr& e) {
1407 out << conn << "(";
1408 unsigned sz = e.num_args();
1409 for (unsigned i = 0; i < sz; ++i) {
1410 display(out, e.arg(i), sz == 1);
1411 if (i + 1 < sz) {
1412 out << ", ";
1413 }
1414 }
1415 out << ")";
1416 }
1417
display_binary(std::ostream & out,char const * conn,z3::expr & e)1418 void display_binary(std::ostream& out, char const* conn, z3::expr& e) {
1419 out << conn << "(";
1420 unsigned sz = e.num_args();
1421 unsigned np = 1;
1422 for (unsigned i = 0; i < sz; ++i) {
1423 display(out, e.arg(i), false);
1424 if (i + 1 < sz) {
1425 out << ", ";
1426 }
1427 if (i + 2 < sz) {
1428 out << conn << "(";
1429 ++np;
1430 }
1431 }
1432 for (unsigned i = 0; i < np; ++i) {
1433 out << ")";
1434 }
1435 }
1436
collect_axiom_ids(named_formulas & axioms)1437 void collect_axiom_ids(named_formulas& axioms) {
1438 m_named_formulas = &axioms;
1439 m_axiom_ids.clear();
1440 for (unsigned i = 0; i < axioms.m_formulas.size(); ++i) {
1441 z3::expr& e = axioms.m_formulas[i];
1442 unsigned id = Z3_get_ast_id(ctx, e);
1443 m_axiom_ids.insert(std::make_pair(id, i));
1444 }
1445 }
1446
display_proof(std::ostream & out,named_formulas & fmls,z3::solver & solver)1447 void display_proof(std::ostream& out, named_formulas& fmls, z3::solver& solver) {
1448 m_node_number = 0;
1449 m_proof_ids.clear();
1450 m_proof_hypotheses.clear();
1451 z3::expr proof = solver.proof();
1452 collect_axiom_ids(fmls);
1453 collect_decls(proof);
1454 collect_hypotheses(proof);
1455 display_sort_decls(out);
1456 display_func_decls(out);
1457 display_proof_rec(out, proof);
1458 }
1459
1460 /**
1461 \brief collect hypotheses for each proof node.
1462 */
collect_hypotheses(z3::expr & proof)1463 void collect_hypotheses(z3::expr& proof) {
1464 Z3_sort proof_sort = proof.get_sort();
1465 size_t todo_size = todo.size();
1466 todo.push_back(proof);
1467 while (todo_size != todo.size()) {
1468 z3::expr p = todo.back();
1469 unsigned id = Z3_get_ast_id(ctx, p);
1470 if (m_proof_hypotheses.find(id) != m_proof_hypotheses.end()) {
1471 todo.pop_back();
1472 continue;
1473 }
1474 bool all_visited = true;
1475 for (unsigned i = 0; i < p.num_args(); ++i) {
1476 z3::expr arg = p.arg(i);
1477 if (arg.get_sort() == proof_sort) {
1478 if (m_proof_hypotheses.find(Z3_get_ast_id(ctx,arg)) == m_proof_hypotheses.end()) {
1479 all_visited = false;
1480 todo.push_back(arg);
1481 }
1482 }
1483 }
1484 if (!all_visited) {
1485 continue;
1486 }
1487 todo.pop_back();
1488 std::set<unsigned> hyps;
1489 if (p.decl().decl_kind() == Z3_OP_PR_LEMMA) {
1490 // we assume here that all hypotheses get consumed in lemmas.
1491 }
1492 else {
1493 for (unsigned i = 0; i < p.num_args(); ++i) {
1494 z3::expr arg = p.arg(i);
1495 if (arg.get_sort() == proof_sort) {
1496 unsigned arg_id = Z3_get_ast_id(ctx,arg);
1497 std::set<unsigned> const& arg_hyps = m_proof_hypotheses.find(arg_id)->second;
1498 std::set<unsigned>::iterator it = arg_hyps.begin(), end = arg_hyps.end();
1499 for (; it != end; ++it) {
1500 hyps.insert(*it);
1501 }
1502 }
1503 }
1504 }
1505 m_proof_hypotheses.insert(std::make_pair(id, hyps));
1506 }
1507
1508 }
1509
display_proof_rec(std::ostream & out,z3::expr proof)1510 unsigned display_proof_rec(std::ostream& out, z3::expr proof) {
1511 Z3_sort proof_sort = proof.get_sort();
1512 size_t todo_size = todo.size();
1513 todo.push_back(proof);
1514 while (todo_size != todo.size()) {
1515 z3::expr p = todo.back();
1516 unsigned id = Z3_get_ast_id(ctx, p);
1517 if (m_proof_ids.find(id) != m_proof_ids.end()) {
1518 todo.pop_back();
1519 continue;
1520 }
1521
1522 switch (p.decl().decl_kind()) {
1523 case Z3_OP_PR_MODUS_PONENS_OEQ: {
1524 unsigned hyp = display_proof_rec(out, p.arg(0));
1525 unsigned num = display_proof_hyp(out, hyp, p.arg(1));
1526 m_proof_ids.insert(std::make_pair(id, num));
1527 todo.pop_back();
1528 continue;
1529 }
1530 default:
1531 break;
1532 }
1533 bool all_visited = true;
1534 for (unsigned i = 0; i < p.num_args(); ++i) {
1535 z3::expr arg = p.arg(i);
1536 if (arg.get_sort() == proof_sort) {
1537 if (m_proof_ids.find(Z3_get_ast_id(ctx,arg)) == m_proof_ids.end()) {
1538 all_visited = false;
1539 todo.push_back(arg);
1540 }
1541 }
1542 }
1543 if (!all_visited) {
1544 continue;
1545 }
1546 todo.pop_back();
1547 unsigned num = ++m_node_number;
1548 m_proof_ids.insert(std::make_pair(id, num));
1549
1550 switch (p.decl().decl_kind()) {
1551 case Z3_OP_PR_ASSERTED: {
1552 std::string formula_name;
1553 std::string formula_file;
1554 unsigned id = Z3_get_ast_id(ctx, p.arg(0));
1555 std::map<unsigned, unsigned>::iterator it = m_axiom_ids.find(id);
1556 if (it != m_axiom_ids.end()) {
1557 formula_name = m_named_formulas->m_names[it->second];
1558 formula_file = m_named_formulas->m_files[it->second];
1559 }
1560 else {
1561 std::ostringstream str;
1562 str << "axiom_" << id;
1563 formula_name = str.str();
1564 formula_file = "unknown";
1565 }
1566 out << "tff(" << m_node_number << ",axiom,(";
1567 display(out, get_proof_formula(p), true);
1568 out << "), file('" << formula_file << "','";
1569 out << formula_name << "')).\n";
1570 break;
1571 }
1572 case Z3_OP_PR_UNDEF:
1573 throw failure_ex("undef rule not handled");
1574 case Z3_OP_PR_TRUE:
1575 display_inference(out, "true", "thm", p);
1576 break;
1577 case Z3_OP_PR_GOAL:
1578 display_inference(out, "goal", "thm", p);
1579 break;
1580 case Z3_OP_PR_MODUS_PONENS:
1581 display_inference(out, "modus_ponens", "thm", p);
1582 break;
1583 case Z3_OP_PR_REFLEXIVITY:
1584 display_inference(out, "reflexivity", "thm", p);
1585 break;
1586 case Z3_OP_PR_SYMMETRY:
1587 display_inference(out, "symmetry", "thm", p);
1588 break;
1589 case Z3_OP_PR_TRANSITIVITY:
1590 case Z3_OP_PR_TRANSITIVITY_STAR:
1591 display_inference(out, "transitivity", "thm", p);
1592 break;
1593 case Z3_OP_PR_MONOTONICITY:
1594 display_inference(out, "monotonicity", "thm", p);
1595 break;
1596 case Z3_OP_PR_QUANT_INTRO:
1597 display_inference(out, "quant_intro", "thm", p);
1598 break;
1599 case Z3_OP_PR_DISTRIBUTIVITY:
1600 display_inference(out, "distributivity", "thm", p);
1601 break;
1602 case Z3_OP_PR_AND_ELIM:
1603 display_inference(out, "and_elim", "thm", p);
1604 break;
1605 case Z3_OP_PR_NOT_OR_ELIM:
1606 display_inference(out, "or_elim", "thm", p);
1607 break;
1608 case Z3_OP_PR_REWRITE:
1609 case Z3_OP_PR_REWRITE_STAR:
1610 display_inference(out, "rewrite", "thm", p);
1611 break;
1612 case Z3_OP_PR_PULL_QUANT:
1613 display_inference(out, "pull_quant", "thm", p);
1614 break;
1615 case Z3_OP_PR_PUSH_QUANT:
1616 display_inference(out, "push_quant", "thm", p);
1617 break;
1618 case Z3_OP_PR_ELIM_UNUSED_VARS:
1619 display_inference(out, "elim_unused_vars", "thm", p);
1620 break;
1621 case Z3_OP_PR_DER:
1622 display_inference(out, "destructive_equality_resolution", "thm", p);
1623 break;
1624 case Z3_OP_PR_QUANT_INST:
1625 display_inference(out, "quant_inst", "thm", p);
1626 break;
1627 case Z3_OP_PR_HYPOTHESIS:
1628 out << "tff(" << m_node_number << ",assumption,(";
1629 display(out, get_proof_formula(p), true);
1630 out << "), introduced(assumption)).\n";
1631 break;
1632 case Z3_OP_PR_LEMMA: {
1633 out << "tff(" << m_node_number << ",plain,(";
1634 display(out, get_proof_formula(p), true);
1635 out << "), inference(lemma,lemma(discharge,";
1636 unsigned parent_id = Z3_get_ast_id(ctx, p.arg(0));
1637 std::set<unsigned> const& hyps = m_proof_hypotheses.find(parent_id)->second;
1638 print_hypotheses(out, hyps);
1639 out << "))).\n";
1640 break;
1641 }
1642 case Z3_OP_PR_UNIT_RESOLUTION:
1643 display_inference(out, "unit_resolution", "thm", p);
1644 break;
1645 case Z3_OP_PR_IFF_TRUE:
1646 display_inference(out, "iff_true", "thm", p);
1647 break;
1648 case Z3_OP_PR_IFF_FALSE:
1649 display_inference(out, "iff_false", "thm", p);
1650 break;
1651 case Z3_OP_PR_COMMUTATIVITY:
1652 display_inference(out, "commutativity", "thm", p);
1653 break;
1654 case Z3_OP_PR_DEF_AXIOM:
1655 display_inference(out, "tautology", "thm", p);
1656 break;
1657 case Z3_OP_PR_DEF_INTRO:
1658 display_inference(out, "def_intro", "sab", p);
1659 break;
1660 case Z3_OP_PR_APPLY_DEF:
1661 display_inference(out, "apply_def", "sab", p);
1662 break;
1663 case Z3_OP_PR_IFF_OEQ:
1664 display_inference(out, "iff_oeq", "sab", p);
1665 break;
1666 case Z3_OP_PR_NNF_POS:
1667 display_inference(out, "nnf_pos", "sab", p);
1668 break;
1669 case Z3_OP_PR_NNF_NEG:
1670 display_inference(out, "nnf_neg", "sab", p);
1671 break;
1672 case Z3_OP_PR_SKOLEMIZE:
1673 display_inference(out, "skolemize", "sab", p);
1674 break;
1675 case Z3_OP_PR_MODUS_PONENS_OEQ:
1676 display_inference(out, "modus_ponens_sab", "sab", p);
1677 break;
1678 case Z3_OP_PR_TH_LEMMA:
1679 display_inference(out, "theory_lemma", "thm", p);
1680 break;
1681 case Z3_OP_PR_HYPER_RESOLVE:
1682 display_inference(out, "hyper_resolve", "thm", p);
1683 break;
1684 case Z3_OP_PR_BIND:
1685 display_inference(out, "bind", "th", p);
1686 break;
1687 default:
1688 out << "TBD: " << m_node_number << "\n" << p << "\n";
1689 throw failure_ex("rule not handled");
1690 }
1691 }
1692 return m_proof_ids.find(Z3_get_ast_id(ctx, proof))->second;
1693 }
1694
display_proof_hyp(std::ostream & out,unsigned hyp,z3::expr p)1695 unsigned display_proof_hyp(std::ostream& out, unsigned hyp, z3::expr p) {
1696 z3::expr fml = p.arg(p.num_args()-1);
1697 z3::expr conclusion = fml.arg(1);
1698 switch (p.decl().decl_kind()) {
1699 case Z3_OP_PR_REFLEXIVITY:
1700 return display_hyp_inference(out, "reflexivity", "sab", conclusion, hyp);
1701 case Z3_OP_PR_IFF_OEQ: {
1702 unsigned hyp2 = display_proof_rec(out, p.arg(0));
1703 return display_hyp_inference(out, "modus_ponens", "thm", conclusion, hyp, hyp2);
1704 }
1705 case Z3_OP_PR_NNF_POS:
1706 case Z3_OP_PR_SKOLEMIZE:
1707 return display_hyp_inference(out, "skolemize", "sab", conclusion, hyp);
1708 case Z3_OP_PR_TRANSITIVITY:
1709 case Z3_OP_PR_TRANSITIVITY_STAR: {
1710 unsigned na = p.num_args();
1711 for (unsigned i = 0; i + 1 < na; ++i) {
1712 if (p.arg(i).num_args() != 2) {
1713 // cop-out: Z3 produces transitivity proofs that are not a chain of equivalences/equi-sats.
1714 // the generated proof is (most likely) not going to be checkable.
1715 continue;
1716 }
1717 z3::expr conclusion = p.arg(i).arg(1);
1718 hyp = display_hyp_inference(out, "transitivity", "sab", conclusion, hyp);
1719 }
1720 return hyp;
1721 }
1722 case Z3_OP_PR_MONOTONICITY:
1723 throw failure_ex("monotonicity rule is not handled");
1724 default:
1725 unsigned hyp2 = 0;
1726 if (p.num_args() == 2) {
1727 hyp2 = display_proof_rec(out, p.arg(0));
1728 }
1729 if (p.num_args() > 2) {
1730 std::cout << "unexpected number of arguments: " << p << "\n";
1731 throw failure_ex("unexpected number of arguments");
1732 }
1733
1734 return display_hyp_inference(out, p.decl().name().str().c_str(), "sab", conclusion, hyp, hyp2);
1735 }
1736 return 0;
1737 }
1738
1739
display_inference(std::ostream & out,char const * name,char const * status,z3::expr p)1740 void display_inference(std::ostream& out, char const* name, char const* status, z3::expr p) {
1741 unsigned id = Z3_get_ast_id(ctx, p);
1742 std::set<unsigned> const& hyps = m_proof_hypotheses.find(id)->second;
1743 out << "tff(" << m_node_number << ",plain,\n (";
1744 display(out, get_proof_formula(p), true);
1745 out << "),\n inference(" << name << ",[status(" << status << ")";
1746 if (!hyps.empty()) {
1747 out << ", assumptions(";
1748 print_hypotheses(out, hyps);
1749 out << ")";
1750 }
1751 out << "],";
1752 display_hypotheses(out, p);
1753 out << ")).\n";
1754 }
1755
print_hypotheses(std::ostream & out,std::set<unsigned> const & hyps)1756 void print_hypotheses(std::ostream& out, std::set<unsigned> const& hyps) {
1757 std::set<unsigned>::iterator it = hyps.begin(), end = hyps.end();
1758 bool first = true;
1759 out << "[";
1760 for (; it != end; ++it) {
1761 if (!first) {
1762 out << ", ";
1763 }
1764 first = false;
1765 out << m_proof_ids.find(*it)->second;
1766 }
1767 out << "]";
1768 }
1769
display_hyp_inference(std::ostream & out,char const * name,char const * status,z3::expr conclusion,unsigned hyp1,unsigned hyp2=0)1770 unsigned display_hyp_inference(std::ostream& out, char const* name, char const* status, z3::expr conclusion, unsigned hyp1, unsigned hyp2 = 0) {
1771 ++m_node_number;
1772 out << "tff(" << m_node_number << ",plain,(\n ";
1773 display(out, conclusion, true);
1774 out << "),\n inference(" << name << ",[status(" << status << ")],";
1775 out << "[" << hyp1;
1776 if (hyp2) {
1777 out << ", " << hyp2;
1778 }
1779 out << "])).\n";
1780 return m_node_number;
1781 }
1782
1783
1784
get_free_vars(z3::expr const & e,std::vector<z3::sort> & vars)1785 void get_free_vars(z3::expr const& e, std::vector<z3::sort>& vars) {
1786 std::set<unsigned> seen;
1787 size_t sz = todo.size();
1788 todo.push_back(e);
1789 while (todo.size() != sz) {
1790 z3::expr e = todo.back();
1791 todo.pop_back();
1792 unsigned id = Z3_get_ast_id(e.ctx(), e);
1793 if (seen.find(id) != seen.end()) {
1794 continue;
1795 }
1796 seen.insert(id);
1797 if (e.is_var()) {
1798 unsigned idx = Z3_get_index_value(ctx, e);
1799 while (idx >= vars.size()) {
1800 vars.push_back(e.get_sort());
1801 }
1802 vars[idx] = e.get_sort();
1803 }
1804 else if (e.is_app()) {
1805 unsigned sz = e.num_args();
1806 for (unsigned i = 0; i < sz; ++i) {
1807 todo.push_back(e.arg(i));
1808 }
1809 }
1810 else {
1811 // e is a quantifier
1812 std::vector<z3::sort> fv;
1813 get_free_vars(e.body(), fv);
1814 unsigned nb = Z3_get_quantifier_num_bound(e.ctx(), e);
1815 for (unsigned i = nb; i < fv.size(); ++i) {
1816 if (vars.size() <= i - nb) {
1817 vars.push_back(fv[i]);
1818 }
1819 }
1820 }
1821 }
1822 }
1823
get_proof_formula(z3::expr proof)1824 z3::expr get_proof_formula(z3::expr proof) {
1825 // unsigned na = proof.num_args();
1826 z3::expr result = proof.arg(proof.num_args()-1);
1827 std::vector<z3::sort> vars;
1828 get_free_vars(result, vars);
1829 if (vars.empty()) {
1830 return result;
1831 }
1832 Z3_sort* sorts = new Z3_sort[vars.size()];
1833 Z3_symbol* names = new Z3_symbol[vars.size()];
1834 for (unsigned i = 0; i < vars.size(); ++i) {
1835 std::ostringstream str;
1836 str << "X" << (i+1);
1837 sorts[vars.size()-i-1] = vars[i];
1838 names[vars.size()-i-1] = Z3_mk_string_symbol(ctx, str.str().c_str());
1839 }
1840 result = z3::expr(ctx, Z3_mk_forall(ctx, 1, 0, 0, static_cast<unsigned>(vars.size()), sorts, names, result));
1841 delete[] sorts;
1842 delete[] names;
1843 return result;
1844 }
1845
display_hypotheses(std::ostream & out,z3::expr p)1846 void display_hypotheses(std::ostream& out, z3::expr p) {
1847 unsigned na = p.num_args();
1848 out << "[";
1849 for (unsigned i = 0; i + 1 < na; ++i) {
1850 out << m_proof_ids.find(Z3_get_ast_id(p.ctx(), p.arg(i)))->second;
1851 if (i + 2 < na) {
1852 out << ", ";
1853 }
1854 }
1855 out << "]";
1856 }
1857
display_sort_decls(std::ostream & out)1858 void display_sort_decls(std::ostream& out) {
1859 for (unsigned i = 0; i < sorts.size(); ++i) {
1860 display_sort_decl(out, sorts[i]);
1861 }
1862 }
1863
display_sort_decl(std::ostream & out,z3::sort & s)1864 void display_sort_decl(std::ostream& out, z3::sort& s) {
1865 out << "tff(" << s << "_type, type, (" << s << ": $tType)).\n";
1866 }
1867
1868
display_func_decls(std::ostream & out)1869 void display_func_decls(std::ostream& out) {
1870 for (size_t i = 0; i < funs.size(); ++i) {
1871 display_func_decl(out, funs[i]);
1872 }
1873 }
1874
contains_id(unsigned id) const1875 bool contains_id(unsigned id) const {
1876 return seen_ids.find(id) != seen_ids.end();
1877 }
1878
collect_decls(z3::expr e)1879 void collect_decls(z3::expr e) {
1880 todo.push_back(e);
1881 while (!todo.empty()) {
1882 z3::expr e = todo.back();
1883 todo.pop_back();
1884 unsigned id = Z3_get_ast_id(ctx, e);
1885 if (contains_id(id)) {
1886 continue;
1887 }
1888 seen_ids.insert(id);
1889 if (e.is_app()) {
1890 collect_fun(e.decl());
1891 unsigned sz = e.num_args();
1892 for (unsigned i = 0; i < sz; ++i) {
1893 todo.push_back(e.arg(i));
1894 }
1895 }
1896 else if (e.is_quantifier()) {
1897 unsigned nb = Z3_get_quantifier_num_bound(e.ctx(), e);
1898 for (unsigned i = 0; i < nb; ++i) {
1899 z3::sort srt(ctx, Z3_get_quantifier_bound_sort(e.ctx(), e, i));
1900 collect_sort(srt);
1901 }
1902 todo.push_back(e.body());
1903 }
1904 else if (e.is_var()) {
1905 collect_sort(e.get_sort());
1906 }
1907 }
1908 }
1909
collect_sort(z3::sort s)1910 void collect_sort(z3::sort s) {
1911 unsigned id = Z3_get_sort_id(ctx, s);
1912 if (s.sort_kind() == Z3_UNINTERPRETED_SORT &&
1913 contains_id(id)) {
1914 seen_ids.insert(id);
1915 sorts.push_back(s);
1916 }
1917 }
1918
collect_fun(z3::func_decl f)1919 void collect_fun(z3::func_decl f) {
1920 unsigned id = Z3_get_func_decl_id(ctx, f);
1921 if (contains_id(id)) {
1922 return;
1923 }
1924 seen_ids.insert(id);
1925 if (f.decl_kind() == Z3_OP_UNINTERPRETED) {
1926 funs.push_back(f);
1927 }
1928 for (unsigned i = 0; i < f.arity(); ++i) {
1929 collect_sort(f.domain(i));
1930 }
1931 collect_sort(f.range());
1932 }
1933
upper_case_var(z3::symbol const & sym)1934 std::string upper_case_var(z3::symbol const& sym) {
1935 std::string result = sanitize(sym);
1936 char ch = result[0];
1937 if ('A' <= ch && ch <= 'Z') {
1938 return result;
1939 }
1940 return "X" + result;
1941 }
1942
lower_case_fun(z3::symbol const & sym)1943 std::string lower_case_fun(z3::symbol const& sym) {
1944 std::string result = sanitize(sym);
1945 char ch = result[0];
1946 if ('a' <= ch && ch <= 'z') {
1947 return result;
1948 }
1949 else {
1950 return "tptp_fun_" + result;
1951 }
1952 }
1953
sanitize(z3::symbol const & sym)1954 std::string sanitize(z3::symbol const& sym) {
1955 std::ostringstream str;
1956 if (sym.kind() == Z3_INT_SYMBOL) {
1957 str << sym;
1958 return str.str();
1959 }
1960 std::string s = sym.str();
1961 size_t sz = s.size();
1962 for (size_t i = 0; i < sz; ++i) {
1963 char ch = s[i];
1964 if ('a' <= ch && ch <= 'z') {
1965 str << ch;
1966 }
1967 else if ('A' <= ch && ch <= 'Z') {
1968 str << ch;
1969 }
1970 else if ('0' <= ch && ch <= '9') {
1971 str << ch;
1972 }
1973 else if ('_' == ch) {
1974 str << ch;
1975 }
1976 else {
1977 str << "_";
1978 }
1979 }
1980 return str.str();
1981 }
1982 };
1983
1984 static char* g_input_file = 0;
1985 static bool g_display_smt2 = false;
1986 static bool g_generate_model = false;
1987 static bool g_generate_proof = false;
1988 static bool g_generate_core = false;
1989 static bool g_display_statistics = false;
1990 static bool g_first_interrupt = true;
1991 static bool g_smt2status = false;
1992 static bool g_check_status = false;
1993 static int g_timeout = 0;
1994 static double g_start_time = 0;
1995 static z3::solver* g_solver = 0;
1996 static z3::context* g_context = 0;
1997 static std::ostream* g_out = &std::cout;
1998
1999
2000
display_usage()2001 static void display_usage() {
2002 unsigned major, minor, build_number, revision_number;
2003 Z3_get_version(&major, &minor, &build_number, &revision_number);
2004 std::cout << "Z3tptp [" << major << "." << minor << "." << build_number << "." << revision_number << "] (c) 2006-20**. Microsoft Corp.\n";
2005 std::cout << "Usage: tptp [options] [-file:]file\n";
2006 std::cout << " -h, -? prints this message.\n";
2007 std::cout << " -smt2 print SMT-LIB2 benchmark.\n";
2008 std::cout << " -m, -model generate model.\n";
2009 std::cout << " -p, -proof generate proof.\n";
2010 std::cout << " -c, -core generate unsat core of named formulas.\n";
2011 std::cout << " -st, -statistics display statistics.\n";
2012 std::cout << " -t:timeout set timeout (in second).\n";
2013 std::cout << " -smt2status display status in smt2 format instead of SZS.\n";
2014 std::cout << " -check_status check the status produced by Z3 against annotation in benchmark.\n";
2015 std::cout << " -<param>:<value> configuration parameter and value.\n";
2016 std::cout << " -o:<output-file> file to place output in.\n";
2017 }
2018
2019
display_statistics()2020 static void display_statistics() {
2021 if (g_solver && g_display_statistics) {
2022 std::cout.flush();
2023 std::cerr.flush();
2024 double end_time = static_cast<double>(clock());
2025 z3::stats stats = g_solver->statistics();
2026 std::cout << stats << "\n";
2027 std::cout << "time: " << (end_time - g_start_time)/CLOCKS_PER_SEC << " secs\n";
2028 }
2029 }
2030
on_ctrl_c(int)2031 static void on_ctrl_c(int) {
2032 if (g_context && g_first_interrupt) {
2033 Z3_interrupt(*g_context);
2034 g_first_interrupt = false;
2035 }
2036 else {
2037 signal (SIGINT, SIG_DFL);
2038 display_statistics();
2039 raise(SIGINT);
2040 }
2041 }
2042
parse_token(char const * & line,char const * token)2043 bool parse_token(char const*& line, char const* token) {
2044 char const* result = line;
2045 while (result[0] == ' ') ++result;
2046 while (token[0] && result[0] == token[0]) {
2047 ++token;
2048 ++result;
2049 }
2050 if (!token[0]) {
2051 line = result;
2052 return true;
2053 }
2054 else {
2055 return false;
2056 }
2057 }
2058
parse_is_sat_line(char const * line,bool & is_sat)2059 bool parse_is_sat_line(char const* line, bool& is_sat) {
2060 if (!parse_token(line, "%")) return false;
2061 if (!parse_token(line, "Status")) return false;
2062 if (!parse_token(line, ":")) return false;
2063
2064 if (parse_token(line, "Unsatisfiable")) {
2065 is_sat = false;
2066 return true;
2067 }
2068 if (parse_token(line, "Theorem")) {
2069 is_sat = false;
2070 return true;
2071 }
2072 if (parse_token(line, "Theorem")) {
2073 is_sat = false;
2074 return true;
2075 }
2076 if (parse_token(line, "CounterSatisfiable")) {
2077 is_sat = true;
2078 return true;
2079 }
2080 if (parse_token(line, "Satisfiable")) {
2081 is_sat = true;
2082 return true;
2083 }
2084 return false;
2085 }
2086
parse_is_sat(char const * filename,bool & is_sat)2087 bool parse_is_sat(char const* filename, bool& is_sat) {
2088 std::ifstream is(filename);
2089 if (is.bad() || is.fail()) {
2090 std::stringstream strm;
2091 strm << "Could not open file " << filename << "\n";
2092 throw failure_ex(strm.str().c_str());
2093 }
2094
2095 for (unsigned i = 0; !is.eof() && i < 200; ++i) {
2096 std::string line;
2097 std::getline(is, line);
2098 if (parse_is_sat_line(line.c_str(), is_sat)) {
2099 return true;
2100 }
2101 }
2102 return false;
2103 }
2104
2105
parse_cmd_line_args(int argc,char ** argv)2106 void parse_cmd_line_args(int argc, char ** argv) {
2107 g_input_file = 0;
2108 g_display_smt2 = false;
2109 int i = 1;
2110 while (i < argc) {
2111 char* arg = argv[i];
2112 //char * eq = 0;
2113 char * opt_arg = 0;
2114 if (arg[0] == '-' || arg[0] == '/') {
2115 ++arg;
2116 while (*arg == '-') {
2117 ++arg;
2118 }
2119 char * colon = strchr(arg, ':');
2120 if (colon) {
2121 opt_arg = colon + 1;
2122 *colon = 0;
2123 }
2124 if (!strcmp(arg,"h") || !strcmp(arg,"help") || !strcmp(arg,"?")) {
2125 display_usage();
2126 exit(0);
2127 }
2128 if (!strcmp(arg,"p") || !strcmp(arg,"proof")) {
2129 g_generate_proof = true;
2130 }
2131 else if (!strcmp(arg,"m") || !strcmp(arg,"model")) {
2132 g_generate_model = true;
2133 }
2134 else if (!strcmp(arg,"c") || !strcmp(arg,"core")) {
2135 g_generate_core = true;
2136 }
2137 else if (!strcmp(arg,"st") || !strcmp(arg,"statistics")) {
2138 g_display_statistics = true;
2139 }
2140 else if (!strcmp(arg,"check_status")) {
2141 g_check_status = true;
2142 }
2143 else if (!strcmp(arg,"t") || !strcmp(arg,"timeout")) {
2144 if (!opt_arg) {
2145 display_usage();
2146 exit(0);
2147 }
2148 g_timeout = atoi(opt_arg);
2149 }
2150 else if (!strcmp(arg,"smt2status")) {
2151 g_smt2status = true;
2152 }
2153 else if (!strcmp(arg,"o")) {
2154 if (opt_arg) {
2155 g_out = new std::ofstream(opt_arg);
2156 if (g_out->bad() || g_out->fail()) {
2157 std::cout << "Could not open file of output: " << opt_arg << "\n";
2158 exit(0);
2159 }
2160 }
2161 else {
2162 display_usage();
2163 exit(0);
2164 }
2165 }
2166 else if (!strcmp(arg,"smt2")) {
2167 g_display_smt2 = true;
2168
2169 }
2170 else if (!strcmp(arg, "file")) {
2171 g_input_file = opt_arg;
2172 }
2173 else if (opt_arg && arg[0] != '"') {
2174 Z3_global_param_set(arg, opt_arg);
2175 }
2176 else {
2177 std::cerr << "parameter " << arg << " was not recognized\n";
2178 display_usage();
2179 exit(0);
2180 }
2181 }
2182 else {
2183 g_input_file = arg;
2184 }
2185 ++i;
2186 }
2187
2188 if (!g_input_file) {
2189 display_usage();
2190 exit(0);
2191 }
2192 }
2193
is_smt2_file(char const * filename)2194 static bool is_smt2_file(char const* filename) {
2195 size_t len = strlen(filename);
2196 return (len > 4 && !strcmp(filename + len - 5,".smt2"));
2197 }
2198
2199
display_tptp(std::ostream & out)2200 static void display_tptp(std::ostream& out) {
2201 // run SMT2 parser, pretty print TFA format.
2202 z3::context ctx;
2203 z3::expr_vector fmls = ctx.parse_file(g_input_file);
2204 z3::expr fml = z3::mk_and(fmls);
2205
2206 pp_tptp pp(ctx);
2207 pp.collect_decls(fml);
2208 pp.display_sort_decls(out);
2209 pp.display_func_decls(out);
2210
2211 if (fml.decl().decl_kind() == Z3_OP_AND) {
2212 for (unsigned i = 0; i < fml.num_args(); ++i) {
2213 pp.display_axiom(out, fml.arg(i));
2214 }
2215 }
2216 else {
2217 pp.display_axiom(out, fml);
2218 }
2219 }
2220
display_proof(z3::context & ctx,named_formulas & fmls,z3::solver & solver)2221 static void display_proof(z3::context& ctx, named_formulas& fmls, z3::solver& solver) {
2222 pp_tptp pp(ctx);
2223 pp.display_proof(std::cout, fmls, solver);
2224 }
2225
display_model(z3::context & ctx,z3::model model)2226 static void display_model(z3::context& ctx, z3::model model) {
2227 unsigned nc = model.num_consts();
2228 unsigned nf = model.num_funcs();
2229 z3::expr_vector fmls(ctx);
2230 for (unsigned i = 0; i < nc; ++i) {
2231 z3::func_decl f = model.get_const_decl(i);
2232 z3::expr e = model.get_const_interp(f);
2233 fmls.push_back(f() == e);
2234 }
2235
2236 for (unsigned i = 0; i < nf; ++i) {
2237 z3::func_decl f = model.get_func_decl(i);
2238 z3::func_interp fi = model.get_func_interp(f);
2239 unsigned arity = f.arity();
2240 z3::expr_vector args(ctx);
2241 for (unsigned j = 0; j < arity; ++j) {
2242 std::ostringstream str;
2243 str << "X" << j;
2244 z3::symbol sym(ctx, Z3_mk_string_symbol(ctx, str.str().c_str()));
2245 args.push_back(ctx.constant(sym, f.domain(j)));
2246 }
2247 unsigned ne = fi.num_entries();
2248 Z3_ast* conds = new Z3_ast[arity];
2249 Z3_ast* conds_match = new Z3_ast[ne];
2250 z3::expr_vector conds_matchv(ctx);
2251 z3::expr els = fi.else_value();
2252 unsigned num_cases = 0;
2253 for (unsigned k = 0; k < ne; ++k) {
2254 z3::func_entry e = fi.entry(k);
2255 z3::expr_vector condv(ctx), args_e(ctx);
2256 if (((Z3_ast)els) && (Z3_get_ast_id(ctx, els) == Z3_get_ast_id(ctx, e.value()))) {
2257 continue;
2258 }
2259 for (unsigned j = 0; j < arity; ++j) {
2260 args_e.push_back(e.arg(j));
2261 condv.push_back(e.arg(j) == args[j]);
2262 conds[j] = condv.back();
2263 }
2264 z3::expr cond(ctx, Z3_mk_and(ctx, arity, conds));
2265 conds_matchv.push_back(cond);
2266 conds_match[num_cases] = cond;
2267 fmls.push_back(f(args_e) == e.value());
2268 ++num_cases;
2269 }
2270 if (els) {
2271 els = f(args) == els;
2272 switch (num_cases) {
2273 case 0: els = forall(args, els); break;
2274 case 1: els = forall(args, implies(!z3::expr(ctx, conds_match[0]), els)); break;
2275 default: els = forall(args, implies(!z3::expr(ctx, Z3_mk_or(ctx, num_cases, conds_match)), els)); break;
2276 }
2277 fmls.push_back(els);
2278 }
2279 delete[] conds;
2280 delete[] conds_match;
2281 }
2282
2283 pp_tptp pp(ctx);
2284 for (unsigned i = 0; i < fmls.size(); ++i) {
2285 pp.collect_decls(fmls[i]);
2286 }
2287 pp.display_sort_decls(std::cout);
2288 pp.display_func_decls(std::cout);
2289 for (unsigned i = 0; i < fmls.size(); ++i) {
2290 pp.display_axiom(std::cout, fmls[i]);
2291 }
2292 }
2293
display_smt2(std::ostream & out)2294 static void display_smt2(std::ostream& out) {
2295 z3::config config;
2296 z3::context ctx(config);
2297 named_formulas fmls;
2298 env env(ctx);
2299 try {
2300 env.parse(g_input_file, fmls);
2301 }
2302 catch (failure_ex& ex) {
2303 std::cerr << ex.msg << "\n";
2304 return;
2305 }
2306
2307 size_t num_assumptions = fmls.m_formulas.size();
2308
2309 Z3_ast* assumptions = new Z3_ast[num_assumptions];
2310 for (size_t i = 0; i < num_assumptions; ++i) {
2311 assumptions[i] = fmls.m_formulas[i];
2312 }
2313 Z3_string s =
2314 Z3_benchmark_to_smtlib_string(
2315 ctx,
2316 "Benchmark generated from TPTP", // comment
2317 0, // no logic is set
2318 "unknown", // no status annotation
2319 "", // attributes
2320 static_cast<unsigned>(num_assumptions),
2321 assumptions,
2322 ctx.bool_val(true));
2323
2324 out << s << "\n";
2325 delete[] assumptions;
2326 }
2327
prove_tptp()2328 static void prove_tptp() {
2329 z3::config config;
2330 if (g_generate_proof) {
2331 config.set("proof", true);
2332 z3::set_param("proof", true);
2333 }
2334 z3::context ctx(config);
2335 z3::solver solver(ctx);
2336 g_solver = &solver;
2337 g_context = &ctx;
2338 if (g_timeout) {
2339 // TBD overflow check
2340 z3::set_param("timeout", g_timeout*1000);
2341 z3::params params(ctx);
2342 params.set("timeout", static_cast<unsigned>(g_timeout*1000));
2343 solver.set(params);
2344 }
2345
2346
2347 named_formulas fmls;
2348 env env(ctx);
2349 try {
2350 env.parse(g_input_file, fmls);
2351 }
2352 catch (failure_ex& ex) {
2353 std::cerr << ex.msg << "\n";
2354 std::cout << "% SZS status GaveUp\n";
2355 return;
2356 }
2357
2358 size_t num_assumptions = fmls.m_formulas.size();
2359
2360 z3::check_result result;
2361
2362 if (g_generate_core) {
2363 z3::expr_vector assumptions(ctx);
2364
2365 for (size_t i = 0; i < num_assumptions; ++i) {
2366 z3::expr pred = ctx.constant(fmls.m_names[i].c_str(), ctx.bool_sort());
2367 z3::expr def = fmls.m_formulas[i] == pred;
2368 solver.add(def);
2369 assumptions.push_back(pred);
2370 }
2371 result = solver.check(assumptions);
2372 }
2373 else {
2374 for (unsigned i = 0; i < num_assumptions; ++i) {
2375 solver.add(fmls.m_formulas[i]);
2376 }
2377 result = solver.check();
2378 }
2379
2380 switch(result) {
2381 case z3::unsat:
2382 if (g_smt2status) {
2383 std::cout << result << "\n";
2384 }
2385 else if (fmls.has_conjecture()) {
2386 std::cout << "% SZS status Theorem\n";
2387 }
2388 else {
2389 std::cout << "% SZS status Unsatisfiable\n";
2390 }
2391 if (g_generate_proof) {
2392 try {
2393 std::cout << "% SZS output start Proof\n";
2394 display_proof(ctx, fmls, solver);
2395 std::cout << "% SZS output end Proof\n";
2396 }
2397 catch (failure_ex& ex) {
2398 std::cerr << "Proof display could not be completed: " << ex.msg << "\n";
2399 }
2400 }
2401 if (g_generate_core) {
2402 z3::expr_vector core = solver.unsat_core();
2403 std::cout << "% SZS core ";
2404 for (unsigned i = 0; i < core.size(); ++i) {
2405 std::cout << core[i] << " ";
2406 }
2407 std::cout << "\n";
2408 }
2409 break;
2410 case z3::sat:
2411 if (g_smt2status) {
2412 std::cout << result << "\n";
2413 }
2414 else if (fmls.has_conjecture()) {
2415 std::cout << "% SZS status CounterSatisfiable\n";
2416 }
2417 else {
2418 std::cout << "% SZS status Satisfiable\n";
2419 }
2420 if (g_generate_model) {
2421 std::cout << "% SZS output start Model\n";
2422 display_model(ctx, solver.get_model());
2423 std::cout << "% SZS output end Model\n";
2424 }
2425 break;
2426 case z3::unknown:
2427 if (g_smt2status) {
2428 std::cout << result << "\n";
2429 }
2430 else if (!g_first_interrupt) {
2431 std::cout << "% SZS status Interrupted\n";
2432 }
2433 else {
2434 std::cout << "% SZS status GaveUp\n";
2435 std::string reason = solver.reason_unknown();
2436 std::cout << "% SZS reason " << reason << "\n";
2437 }
2438 break;
2439 }
2440 bool is_sat = true;
2441 if (g_check_status &&
2442 result != z3::unknown &&
2443 parse_is_sat(g_input_file, is_sat)) {
2444 if (is_sat && result == z3::unsat) {
2445 std::cout << "BUG!! expected result is Satisfiable, returned result is Unsat\n";
2446 }
2447 if (!is_sat && result == z3::sat) {
2448 std::cout << "BUG!! expected result is Unsatisfiable, returned result is Satisfiable\n";
2449 }
2450 }
2451 display_statistics();
2452 }
2453
main(int argc,char ** argv)2454 int main(int argc, char** argv) {
2455
2456 g_start_time = static_cast<double>(clock());
2457 signal(SIGINT, on_ctrl_c);
2458
2459 parse_cmd_line_args(argc, argv);
2460
2461 if (is_smt2_file(g_input_file)) {
2462 display_tptp(*g_out);
2463 }
2464 else if (g_display_smt2) {
2465 display_smt2(*g_out);
2466 }
2467 else {
2468 try {
2469 prove_tptp();
2470 }
2471 catch (z3::exception& ex) {
2472 std::cerr << "Exception during proof: " << ex.msg() << "\n";
2473 }
2474 }
2475 return 0;
2476 }
2477
2478