mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
fix build
This commit is contained in:
parent
006418e027
commit
ca97bfb4b8
|
@ -2,7 +2,7 @@
|
|||
Copyright (c) 2015 Microsoft Corporation
|
||||
--*/
|
||||
|
||||
#ifndef Z3_API_H_
|
||||
#pragma once
|
||||
|
||||
DEFINE_TYPE(Z3_symbol);
|
||||
DEFINE_TYPE(Z3_literals);
|
||||
|
@ -5557,12 +5557,12 @@ extern "C" {
|
|||
*/
|
||||
|
||||
Z3_string Z3_API Z3_eval_smtlib2_string(Z3_context, Z3_string str);
|
||||
|
||||
|
||||
/*@}*/
|
||||
|
||||
/** @name Error Handling */
|
||||
/*@{*/
|
||||
#pragma once
|
||||
#ifndef SAFE_ERRORS
|
||||
/**
|
||||
\brief Return the error code for the last API call.
|
||||
|
||||
|
|
|
@ -16,7 +16,7 @@ Author:
|
|||
Revision History:
|
||||
|
||||
--*/
|
||||
#ifndef SMT_ENODE_H_
|
||||
#pragma once
|
||||
|
||||
#include "ast/ast.h"
|
||||
#include "smt/smt_types.h"
|
||||
|
@ -46,7 +46,7 @@ namespace smt {
|
|||
|
||||
// #define SPARSE_MAP
|
||||
|
||||
#pragma once
|
||||
#ifndef SPARSE_MAP
|
||||
typedef ptr_vector<enode> app2enode_t; // app -> enode
|
||||
#else
|
||||
class app2enode_t : public u_map<enode *> {
|
||||
|
|
|
@ -16,7 +16,7 @@ Author:
|
|||
Revision History:
|
||||
|
||||
--*/
|
||||
#ifndef MPQ_INF_H_
|
||||
#pragma once
|
||||
|
||||
#include "util/mpq.h"
|
||||
#include "util/hash.h"
|
||||
|
@ -39,14 +39,14 @@ public:
|
|||
}
|
||||
|
||||
enum inf_kind { NEG=-1, ZERO, POS };
|
||||
|
||||
|
||||
void reset(mpq_inf & a) {
|
||||
m.reset(a.first);
|
||||
m.reset(a.second);
|
||||
}
|
||||
|
||||
|
||||
unsigned hash(mpq_inf const & a) const { return hash_u_u(m.hash(a.first), m.hash(a.second)); }
|
||||
|
||||
|
||||
void del(mpq_inf & a) {
|
||||
m.del(a.first);
|
||||
m.del(a.second);
|
||||
|
@ -278,7 +278,7 @@ public:
|
|||
mpq_manager<SYNCH>& get_mpq_manager() { return m; }
|
||||
};
|
||||
|
||||
#pragma once
|
||||
#ifndef SINGLE_THREAD
|
||||
typedef mpq_inf_manager<true> synch_mpq_inf_manager;
|
||||
#else
|
||||
typedef mpq_inf_manager<false> synch_mpq_inf_manager;
|
||||
|
|
Loading…
Reference in a new issue