Skip to content

Commit

Permalink
fix build of tests
Browse files Browse the repository at this point in the history
  • Loading branch information
nunoplopes committed Jun 17, 2022
1 parent fcbbf7b commit c3407fc
Show file tree
Hide file tree
Showing 67 changed files with 67 additions and 6 deletions.
1 change: 1 addition & 0 deletions src/test/algebraic.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,7 @@ Module Name:
#include "math/polynomial/polynomial_var2value.h"
#include "util/mpbq.h"
#include "util/rlimit.h"
#include <iostream>

static void display_anums(std::ostream & out, scoped_anum_vector const & rs) {
out << "numbers in decimal:\n";
Expand Down
2 changes: 1 addition & 1 deletion src/test/arith_rewriter.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ Copyright (c) 2015 Microsoft Corporation
#include "ast/rewriter/th_rewriter.h"
#include "model/model.h"
#include "parsers/smt2/smt2parser.h"

#include <iostream>

static expr_ref parse_fml(ast_manager& m, char const* str) {
expr_ref result(m);
Expand Down
1 change: 1 addition & 0 deletions src/test/arith_simplifier_plugin.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ Copyright (c) 2015 Microsoft Corporation

#include "smt/arith_eq_solver.h"
#include "smt/params/smt_params.h"
#include <iostream>

typedef rational numeral;
typedef vector<numeral> row;
Expand Down
1 change: 1 addition & 0 deletions src/test/bdd.cpp
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
#include "math/dd/dd_bdd.h"
#include <iostream>

namespace dd {
static void test1() {
Expand Down
1 change: 1 addition & 0 deletions src/test/bits.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,7 @@ Copyright (c) 2015 Microsoft Corporation
#include "util/vector.h"
#include "util/mpz.h"
#include "util/bit_util.h"
#include <iostream>

static void tst_shl(unsigned src_sz, unsigned const * src, unsigned k,
unsigned dst_sz, unsigned const * dst, bool trace = true) {
Expand Down
1 change: 1 addition & 0 deletions src/test/chashtable.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,7 @@ Revision History:
#include "util/hashtable.h"
#include "util/hash.h"
#include "util/util.h"
#include <iostream>

typedef chashtable<int, int_hash, default_eq<int> > int_table;
typedef cmap<int, int, int_hash, default_eq<int> > int_map;
Expand Down
2 changes: 1 addition & 1 deletion src/test/cube_clause.cpp
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
#include "ast/reg_decl_plugins.h"
#include "solver/solver_pool.h"
#include "smt/smt_solver.h"

#include <iostream>

void tst_cube_clause() {
ast_manager m;
Expand Down
1 change: 1 addition & 0 deletions src/test/datalog_parser.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@ Copyright (c) 2015 Microsoft Corporation
#include "muz/fp/dl_register_engine.h"
#include "smt/params/smt_params.h"
#include "ast/reg_decl_plugins.h"
#include <iostream>

using namespace datalog;

Expand Down
1 change: 1 addition & 0 deletions src/test/dl_query.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@ Copyright (c) 2015 Microsoft Corporation
#include "util/stopwatch.h"
#include "ast/reg_decl_plugins.h"
#include "muz/rel/dl_relation_manager.h"
#include <iostream>

using namespace datalog;

Expand Down
1 change: 1 addition & 0 deletions src/test/dl_table.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ Copyright (c) 2015 Microsoft Corporation
#include "muz/rel/dl_table.h"
#include "muz/fp/dl_register_engine.h"
#include "muz/rel/dl_relation_manager.h"
#include <iostream>

typedef datalog::table_base* (*mk_table_fn)(datalog::relation_manager& m, datalog::table_signature& sig);

Expand Down
2 changes: 1 addition & 1 deletion src/test/doc.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ Copyright (c) 2015 Microsoft Corporation
#include "ast/ast_util.h"
#include "ast/rewriter/expr_safe_replace.h"
#include "ast/rewriter/th_rewriter.h"

#include <iostream>

static void tst_doc1(unsigned n) {
doc_manager m(n);
Expand Down
1 change: 1 addition & 0 deletions src/test/egraph.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@ Copyright (c) 2020 Microsoft Corporation
#include "ast/reg_decl_plugins.h"
#include "ast/ast_pp.h"
#include "ast/arith_decl_plugin.h"
#include <iostream>

static expr_ref mk_const(ast_manager& m, char const* name, sort* s) {
return expr_ref(m.mk_const(symbol(name), s), m);
Expand Down
1 change: 1 addition & 0 deletions src/test/escaped.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,7 @@ Revision History:
--*/
#include "util/util.h"
#include <iostream>

void tst_escaped() {
std::cout << "[" << escaped("\"hello\"\"world\"\n\n") << "]\n";
Expand Down
1 change: 1 addition & 0 deletions src/test/expr_substitution.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@ Copyright (c) 2015 Microsoft Corporation
#include "ast/arith_decl_plugin.h"
#include "ast/reg_decl_plugins.h"
#include "ast/rewriter/th_rewriter.h"
#include <iostream>

expr* mk_bv_xor(bv_util& bv, expr* a, expr* b) {
expr* args[2];
Expand Down
1 change: 1 addition & 0 deletions src/test/f2n.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,7 @@ Revision History:
#include "util/f2n.h"
#include "util/hwf.h"
#include "util/mpf.h"
#include <iostream>

static void tst1() {
hwf_manager hm;
Expand Down
1 change: 1 addition & 0 deletions src/test/factor_rewriter.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@ Copyright (c) 2015 Microsoft Corporation
#include "ast/bv_decl_plugin.h"
#include "ast/ast_pp.h"
#include "ast/reg_decl_plugins.h"
#include <iostream>

void tst_factor_rewriter() {
ast_manager m;
Expand Down
1 change: 1 addition & 0 deletions src/test/get_consequences.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@ Copyright (c) 2016 Microsoft Corporation
#include "tactic/tactic.h"
#include "model/model_smt2_pp.h"
#include "tactic/fd_solver/fd_solver.h"
#include <iostream>

static expr_ref mk_const(ast_manager& m, char const* name, sort* s) {
return expr_ref(m.mk_const(symbol(name), s), m);
Expand Down
1 change: 1 addition & 0 deletions src/test/heap_trie.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@ Copyright (c) 2015 Microsoft Corporation
--*/

#include "math/hilbert/heap_trie.h"
#include <iostream>

struct unsigned_le {
static bool le(unsigned i, unsigned j) { return i <= j; }
Expand Down
1 change: 1 addition & 0 deletions src/test/hilbert_basis.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@ Copyright (c) 2015 Microsoft Corporation
#include "util/rlimit.h"
#include <signal.h>
#include <time.h>
#include <iostream>
#include <sstream>

static bool g_use_ordered_support = false;
Expand Down
1 change: 1 addition & 0 deletions src/test/horn_subsume_model_converter.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@ Copyright (c) 2015 Microsoft Corporation
#include "ast/arith_decl_plugin.h"
#include "model/model_smt2_pp.h"
#include "ast/reg_decl_plugins.h"
#include <iostream>

void tst_horn_subsume_model_converter() {
ast_manager m;
Expand Down
1 change: 1 addition & 0 deletions src/test/hwf.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,7 @@ Revision History:
#include "util/hwf.h"
#include "util/f2n.h"
#include "util/rational.h"
#include <iostream>

static void bug_set_double() {
hwf_manager m;
Expand Down
1 change: 1 addition & 0 deletions src/test/interval.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,7 @@ Revision History:
#include "ast/ast.h"
#include "util/debug.h"
#include "util/rlimit.h"
#include <iostream>

template class interval_manager<im_default_config>;
typedef im_default_config::interval interval;
Expand Down
1 change: 1 addition & 0 deletions src/test/karr.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@ Copyright (c) 2015 Microsoft Corporation
--*/
#include "util/rlimit.h"
#include "math/hilbert/hilbert_basis.h"
#include <iostream>

/*
Test generation of linear congruences a la Karr.
Expand Down
1 change: 1 addition & 0 deletions src/test/model2expr.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@ Copyright (c) 2015 Microsoft Corporation
#include "ast/arith_decl_plugin.h"
#include "model/model_smt2_pp.h"
#include "ast/reg_decl_plugins.h"
#include <iostream>

void tst_model2expr() {
ast_manager m;
Expand Down
1 change: 1 addition & 0 deletions src/test/model_based_opt.cpp
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
#include "math/simplex/model_based_opt.h"
#include "util/util.h"
#include "util/uint_set.h"
#include <iostream>

typedef opt::model_based_opt::var var;

Expand Down
2 changes: 1 addition & 1 deletion src/test/model_evaluator.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
#include "ast/arith_decl_plugin.h"
#include "ast/reg_decl_plugins.h"
#include "ast/ast_pp.h"

#include <iostream>

void tst_model_evaluator() {
ast_manager m;
Expand Down
1 change: 1 addition & 0 deletions src/test/model_retrieval.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@ Copyright (c) 2015 Microsoft Corporation
#include "ast/array_decl_plugin.h"
#include "model/model_v2_pp.h"
#include "ast/reg_decl_plugins.h"
#include <iostream>

void tst_model_retrieval()
{
Expand Down
1 change: 1 addition & 0 deletions src/test/mpbq.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,7 @@ Revision History:
--*/
#include "util/mpbq.h"
#include <iostream>

static void tst1() {
unsynch_mpz_manager zm;
Expand Down
1 change: 1 addition & 0 deletions src/test/mpff.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,7 @@ Revision History:
--*/
#include <sstream>
#include <cstring>
#include <iostream>
#include "util/mpff.h"
#include "util/mpz.h"
#include "util/mpq.h"
Expand Down
1 change: 1 addition & 0 deletions src/test/mpfx.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,7 @@ Revision History:
--*/
#include "util/mpfx.h"
#include <iostream>

static void tst1() {
mpfx_manager m;
Expand Down
1 change: 1 addition & 0 deletions src/test/mpq.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,7 @@ Revision History:
#include "util/mpq.h"
#include "util/rational.h"
#include "util/timeit.h"
#include <iostream>

static void tst0() {
synch_mpq_manager m;
Expand Down
1 change: 1 addition & 0 deletions src/test/mpz.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,7 @@ Revision History:
#include "util/rational.h"
#include "util/timeit.h"
#include "util/scoped_numeral.h"
#include <iostream>

static void tst1() {
synch_mpz_manager m;
Expand Down
1 change: 1 addition & 0 deletions src/test/nlarith_util.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@ Copyright (c) 2015 Microsoft Corporation
#include "ast/arith_decl_plugin.h"
#include "ast/ast_pp.h"
#include "ast/reg_decl_plugins.h"
#include <iostream>

void tst_nlarith_util() {
ast_manager M;
Expand Down
1 change: 1 addition & 0 deletions src/test/nlsat.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -24,6 +24,7 @@ Module Name:
#include "nlsat/nlsat_explain.h"
#include "math/polynomial/polynomial_cache.h"
#include "util/rlimit.h"
#include <iostream>

nlsat::interval_set_ref tst_interval(nlsat::interval_set_ref const & s1,
nlsat::interval_set_ref const & s2,
Expand Down
1 change: 1 addition & 0 deletions src/test/old_interval.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,7 @@ Revision History:
--*/
#include "smt/old_interval.h"
#include <iostream>

static void tst1() {
ext_numeral inf(true);
Expand Down
1 change: 1 addition & 0 deletions src/test/parray.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,7 @@ Revision History:
#include "util/parray.h"
#include "util/small_object_allocator.h"
#include "ast/ast.h"
#include <iostream>

template<bool PRESERVE_ROOTS>
struct int_parray_config {
Expand Down
1 change: 1 addition & 0 deletions src/test/pb2bv.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,7 @@ Copyright (c) 2015 Microsoft Corporation
#include "tactic/fd_solver/fd_solver.h"
#include "solver/solver.h"
#include "ast/arith_decl_plugin.h"
#include <iostream>

static void test1() {
ast_manager m;
Expand Down
1 change: 1 addition & 0 deletions src/test/pdd.cpp
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
#include "math/dd/dd_pdd.h"
#include <iostream>

namespace dd {

Expand Down
1 change: 1 addition & 0 deletions src/test/pdd_solver.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@
#include "tactic/goal.h"
#include "tactic/tactic.h"
#include "tactic/bv/bit_blaster_tactic.h"
#include <iostream>

namespace dd {
void print_eqs(ptr_vector<solver::equation> const& eqs) {
Expand Down
1 change: 1 addition & 0 deletions src/test/polynomial.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,7 @@ Module Name:
#include "math/polynomial/polynomial_cache.h"
#include "math/polynomial/linear_eq_solver.h"
#include "util/rlimit.h"
#include <iostream>

static void tst1() {
std::cout << "\n----- Basic testing -------\n";
Expand Down
2 changes: 1 addition & 1 deletion src/test/polynorm.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ Copyright (c) 2015 Microsoft Corporation
#include "ast/reg_decl_plugins.h"
#include "ast/rewriter/arith_rewriter.h"
#include "ast/ast_pp.h"

#include <iostream>

static expr_ref parse_fml(ast_manager& m, char const* str) {
expr_ref result(m);
Expand Down
1 change: 1 addition & 0 deletions src/test/prime_generator.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,7 @@ Module Name:
--*/
#include "util/mpz.h"
#include "util/prime_generator.h"
#include <iostream>

void tst_prime_generator() {
unsynch_mpz_manager m;
Expand Down
1 change: 1 addition & 0 deletions src/test/proof_checker.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ Copyright (c) 2015 Microsoft Corporation

#include "ast/proofs/proof_checker.h"
#include "ast/ast_ll_pp.h"
#include <iostream>

void tst_checker1() {
ast_manager m(PGM_ENABLED);
Expand Down
1 change: 1 addition & 0 deletions src/test/qe_arith.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@ Copyright (c) 2015 Microsoft Corporation
#include "smt/smt_context.h"
#include "ast/expr_abstract.h"
#include "ast/rewriter/expr_safe_replace.h"
#include <iostream>

static expr_ref parse_fml(ast_manager& m, char const* str) {
expr_ref result(m);
Expand Down
1 change: 1 addition & 0 deletions src/test/quant_solve.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,7 @@ Copyright (c) 2015 Microsoft Corporation
#include "model/model_smt2_pp.h"
#include "parsers/smt2/smt2parser.h"
#include "ast/rewriter/var_subst.h"
#include <iostream>

static void validate_quant_solution(ast_manager& m, expr* fml, expr* guard, qe::def_vector const& defs) {
// verify:
Expand Down
1 change: 1 addition & 0 deletions src/test/rcf.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,7 @@ Module Name:
#include "math/realclosure/realclosure.h"
#include "math/realclosure/mpz_matrix.h"
#include "util/rlimit.h"
#include <iostream>

static void tst1() {
unsynch_mpq_manager qm;
Expand Down
1 change: 1 addition & 0 deletions src/test/sat_local_search.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@
#include "util/cancel_eh.h"
#include "util/scoped_ctrl_c.h"
#include "util/scoped_timer.h"
#include <iostream>

static bool build_instance(char const * filename, sat::solver& s, sat::local_search& local_search)
{
Expand Down
1 change: 1 addition & 0 deletions src/test/sat_lookahead.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@
#include "util/statistics.h"
#include "sat/sat_lookahead.h"
#include "sat/dimacs.h"
#include <iostream>

static void display_model(sat::model const & m) {
for (unsigned i = 1; i < m.size(); i++) {
Expand Down
1 change: 1 addition & 0 deletions src/test/sat_user_scope.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ Copyright (c) 2015 Microsoft Corporation

#include "sat/sat_solver.h"
#include "util/util.h"
#include <iostream>

typedef sat::literal_vector clause_t;
typedef vector<clause_t> clauses_t;
Expand Down
Loading

0 comments on commit c3407fc

Please sign in to comment.