mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

fix build

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-03-10 11:39:22 -08:00
parent 6e87622c8a
commit 0ce2001449
2 changed files with 7 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
examples/tptp/tptp5.cpp
View file

@ -1609,7 +1609,6 @@ public:
display_inference(out, "rewrite", "thm", p); display_inference(out, "rewrite", "thm", p);
break; break;
case Z3_OP_PR_PULL_QUANT: case Z3_OP_PR_PULL_QUANT:
case Z3_OP_PR_PULL_QUANT_STAR:
display_inference(out, "pull_quant", "thm", p); display_inference(out, "pull_quant", "thm", p);
break; break;
case Z3_OP_PR_PUSH_QUANT: case Z3_OP_PR_PUSH_QUANT:
@ -1669,12 +1668,6 @@ public:
case Z3_OP_PR_NNF_NEG: case Z3_OP_PR_NNF_NEG:
display_inference(out, "nnf_neg", "sab", p); display_inference(out, "nnf_neg", "sab", p);
break; break;
case Z3_OP_PR_NNF_STAR:
display_inference(out, "nnf", "sab", p);
break;
case Z3_OP_PR_CNF_STAR:
display_inference(out, "cnf", "sab", p);
break;
case Z3_OP_PR_SKOLEMIZE: case Z3_OP_PR_SKOLEMIZE:
display_inference(out, "skolemize", "sab", p); display_inference(out, "skolemize", "sab", p);
break; break;
@ -1706,10 +1699,6 @@ public:
return display_hyp_inference(out, "modus_ponens", "thm", conclusion, hyp, hyp2); return display_hyp_inference(out, "modus_ponens", "thm", conclusion, hyp, hyp2);
} }
case Z3_OP_PR_NNF_POS: case Z3_OP_PR_NNF_POS:
case Z3_OP_PR_NNF_STAR:
return display_hyp_inference(out, "nnf", "sab", conclusion, hyp);
case Z3_OP_PR_CNF_STAR:
return display_hyp_inference(out, "cnf", "sab", conclusion, hyp);
case Z3_OP_PR_SKOLEMIZE: case Z3_OP_PR_SKOLEMIZE:
return display_hyp_inference(out, "skolemize", "sab", conclusion, hyp); return display_hyp_inference(out, "skolemize", "sab", conclusion, hyp);
case Z3_OP_PR_TRANSITIVITY: case Z3_OP_PR_TRANSITIVITY:

9
scripts/mk_util.py
View file

@ -889,8 +889,13 @@ def is_CXX_gpp():
return is_compiler(CXX, 'g++') return is_compiler(CXX, 'g++')
def is_clang_in_gpp_form(cc): def is_clang_in_gpp_form(cc):
version_string = check_output([cc, '--version']).encode('utf-8').decode('utf-8') str = check_output([cc, '--version'])
return version_string.find('clang') != -1 try:
version_string = str.encode('utf-8')
except:
version_string = str
clang = 'clang'.encode('utf-8')
return version_string.find(clang) != -1
def is_CXX_clangpp(): def is_CXX_clangpp():
if is_compiler(CXX, 'g++'): if is_compiler(CXX, 'g++'):