mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 01:24:08 +00:00
fix python build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
eca250933d
commit
ad92bfb1a1
|
@ -11,10 +11,10 @@ from mk_util import *
|
|||
def init_project_def():
|
||||
set_version(4, 5, 1, 0)
|
||||
add_lib('util', [])
|
||||
add_lib('lp', ['util'], 'util/lp')
|
||||
add_lib('polynomial', ['util'], 'math/polynomial')
|
||||
add_lib('sat', ['util'])
|
||||
add_lib('nlsat', ['polynomial', 'sat'])
|
||||
add_lib('lp', ['util','nlsat'], 'util/lp')
|
||||
add_lib('hilbert', ['util'], 'math/hilbert')
|
||||
add_lib('simplex', ['util'], 'math/simplex')
|
||||
add_lib('automata', ['util'], 'math/automata')
|
||||
|
@ -69,10 +69,9 @@ def init_project_def():
|
|||
add_lib('ddnf', ['muz', 'transforms', 'rel'], 'muz/ddnf')
|
||||
add_lib('duality_intf', ['muz', 'transforms', 'duality'], 'muz/duality')
|
||||
add_lib('fp', ['muz', 'pdr', 'clp', 'tab', 'rel', 'bmc', 'duality_intf', 'ddnf', 'spacer'], 'muz/fp')
|
||||
add_lib('nlsat_smt_tactic', ['nlsat_tactic', 'smt_tactic'], 'tactic/nlsat_smt')
|
||||
add_lib('ufbv_tactic', ['normal_forms', 'core_tactics', 'macros', 'smt_tactic', 'rewriter'], 'tactic/ufbv')
|
||||
add_lib('sat_solver', ['solver', 'core_tactics', 'aig_tactic', 'bv_tactics', 'arith_tactics', 'sat_tactic'], 'sat/sat_solver')
|
||||
add_lib('smtlogic_tactics', ['ackermannization', 'sat_solver', 'arith_tactics', 'bv_tactics', 'nlsat_tactic', 'smt_tactic', 'aig_tactic', 'fp', 'muz','qe','nlsat_smt_tactic'], 'tactic/smtlogics')
|
||||
add_lib('smtlogic_tactics', ['ackermannization', 'sat_solver', 'arith_tactics', 'bv_tactics', 'nlsat_tactic', 'smt_tactic', 'aig_tactic', 'fp', 'muz','qe'], 'tactic/smtlogics')
|
||||
add_lib('fpa_tactics', ['fpa', 'core_tactics', 'bv_tactics', 'sat_tactic', 'smt_tactic', 'arith_tactics', 'smtlogic_tactics'], 'tactic/fpa')
|
||||
add_lib('portfolio', ['smtlogic_tactics', 'sat_solver', 'ufbv_tactic', 'fpa_tactics', 'aig_tactic', 'fp', 'qe','sls_tactic', 'subpaving_tactic'], 'tactic/portfolio')
|
||||
add_lib('smtparser', ['portfolio'], 'parsers/smt')
|
||||
|
|
|
@ -19,7 +19,6 @@ Revision History:
|
|||
|
||||
#include "sat/ba_solver.h"
|
||||
#include "sat/sat_types.h"
|
||||
#include "util/lp/lar_solver.h"
|
||||
|
||||
|
||||
namespace sat {
|
||||
|
|
|
@ -30,7 +30,6 @@ Notes:
|
|||
#include "tactic/fpa/qffp_tactic.h"
|
||||
#include "tactic/smtlogics/qfaufbv_tactic.h"
|
||||
#include "tactic/smtlogics/qfauflia_tactic.h"
|
||||
#include "tactic/smtlogics/qfufnra_tactic.h"
|
||||
|
||||
tactic * mk_default_tactic(ast_manager & m, params_ref const & p) {
|
||||
tactic * st = using_params(and_then(mk_simplify_tactic(m),
|
||||
|
|
|
@ -36,7 +36,6 @@ Notes:
|
|||
#include "tactic/portfolio/fd_solver.h"
|
||||
#include "tactic/ufbv/ufbv_tactic.h"
|
||||
#include "tactic/fpa/qffp_tactic.h"
|
||||
#include "tactic/smtlogics/qfufnra_tactic.h"
|
||||
#include "muz/fp/horn_tactic.h"
|
||||
#include "smt/smt_solver.h"
|
||||
#include "sat/sat_solver/inc_sat_solver.h"
|
||||
|
|
|
@ -1,50 +0,0 @@
|
|||
/*++
|
||||
Copyright (c) 2015 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
qfufnra_tactic.cpp
|
||||
|
||||
Abstract:
|
||||
|
||||
Tactic for QF_UFNRA
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj (nbjorner) 2015-05-05
|
||||
|
||||
Notes:
|
||||
|
||||
--*/
|
||||
#include "tactic/tactical.h"
|
||||
#include "tactic/core/simplify_tactic.h"
|
||||
#include "tactic/core/propagate_values_tactic.h"
|
||||
#include "tactic/nlsat_smt/nl_purify_tactic.h"
|
||||
#include "tactic/smtlogics/qfufnra_tactic.h"
|
||||
#include "tactic/arith/purify_arith_tactic.h"
|
||||
#include "tactic/core/solve_eqs_tactic.h"
|
||||
#include "tactic/core/elim_term_ite_tactic.h"
|
||||
#include "tactic/core/elim_uncnstr_tactic.h"
|
||||
#include "tactic/core/simplify_tactic.h"
|
||||
#include "tactic/core/nnf_tactic.h"
|
||||
#include "tactic/core/tseitin_cnf_tactic.h"
|
||||
|
||||
tactic * mk_qfufnra_tactic(ast_manager & m, params_ref const& p) {
|
||||
params_ref main_p = p;
|
||||
main_p.set_bool("elim_and", true);
|
||||
main_p.set_bool("blast_distinct", true);
|
||||
|
||||
return and_then(and_then(using_params(mk_simplify_tactic(m, p), main_p),
|
||||
mk_purify_arith_tactic(m, p),
|
||||
mk_propagate_values_tactic(m, p),
|
||||
mk_solve_eqs_tactic(m, p),
|
||||
mk_elim_uncnstr_tactic(m, p)),
|
||||
and_then(mk_elim_term_ite_tactic(m, p),
|
||||
mk_solve_eqs_tactic(m, p),
|
||||
using_params(mk_simplify_tactic(m, p), main_p),
|
||||
mk_tseitin_cnf_core_tactic(m, p),
|
||||
using_params(mk_simplify_tactic(m, p), main_p),
|
||||
mk_nl_purify_tactic(m, p)));
|
||||
}
|
||||
|
||||
|
|
@ -1,31 +0,0 @@
|
|||
/*++
|
||||
Copyright (c) 2012 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
qfufnra_tactic.h
|
||||
|
||||
Abstract:
|
||||
|
||||
Tactic for QF_UFNRA
|
||||
|
||||
Author:
|
||||
|
||||
Leonardo (leonardo) 2012-02-28
|
||||
|
||||
Notes:
|
||||
|
||||
--*/
|
||||
#ifndef QFUFNRA_TACTIC_H_
|
||||
#define QFUFNRA_TACTIC_H_
|
||||
|
||||
#include "util/params.h"
|
||||
class ast_manager;
|
||||
class tactic;
|
||||
|
||||
tactic * mk_qfufnra_tactic(ast_manager & m, params_ref const & p = params_ref());
|
||||
/*
|
||||
ADD_TACTIC("qfufnra", "builtin strategy for solving QF_UNFRA problems.", "mk_qfufnra_tactic(m, p)")
|
||||
*/
|
||||
|
||||
#endif
|
|
@ -183,7 +183,7 @@ unsigned long long memory::get_max_used_memory() {
|
|||
}
|
||||
|
||||
#if defined(_WINDOWS)
|
||||
#include "Windows.h"
|
||||
#include <Windows.h>
|
||||
#endif
|
||||
|
||||
unsigned long long memory::get_max_memory_size() {
|
||||
|
|
|
@ -18,7 +18,7 @@ Revision History:
|
|||
--*/
|
||||
|
||||
#ifdef _WINDOWS
|
||||
#include "windows.h"
|
||||
#include <windows.h>
|
||||
#endif
|
||||
#include "util/util.h"
|
||||
|
||||
|
|
Loading…
Reference in a new issue