diff --git a/src/test/ast_pp.cpp b/src/test/ast_pp.cpp deleted file mode 100644 index 414b26411..000000000 --- a/src/test/ast_pp.cpp +++ /dev/null @@ -1,59 +0,0 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - tst_ast_pp.cpp - -Abstract: - - Test AST Pretty printing module - -Author: - - Nikolaj Bjorner (nbjorner) 2006-10-5 - -Revision History: - ---*/ -#include "ast.h" -#include "ast_pp.h" -#include "ast_dag_pp.h" -#include "smtparser.h" -#include - -void tst_ast_pp() -{ - ast_manager m; - smtlib::parser* parser = smtlib::parser::create(m); - - parser->initialize_smtlib(); - - - if (!parser->parse_string( - "(benchmark test :extrasorts (A B) :extrafuns ((f A A) (g A A A) (x A) (p A bool)) \n" - ":formula (p (f x))\n" - ":extrafuns ((x1 Int) (y1 Int))\n" - ":formula (<= 1 (+ x1 y1))\n" - ":formula (let (x (g x x)) (let (x (g x x)) (let (x (g x x)) (let (x (g x x)) (p (g x x))))))\n" - ":formula (p x)\n" - ")")) { - SASSERT(false); - dealloc(parser); - return; - } - - smtlib::benchmark* b = parser->get_benchmark(); - - for (unsigned j = 0; j < b->get_num_assumptions(); ++j) { - expr* e = b->get_assumptions()[j]; - std::cout << mk_pp(e, m) << "\n"; - ast_dag_pp(std::cout, m, e); - } - for (unsigned j = 0; j < b->get_num_formulas(); ++j) { - expr* e = b->begin_formulas()[j]; - std::cout << mk_pp(e, m) << "\n"; - ast_dag_pp(std::cout, m, e); - } - dealloc(parser); -} diff --git a/src/test/ast_smt_pp.cpp b/src/test/ast_smt_pp.cpp deleted file mode 100644 index 05fd5748e..000000000 --- a/src/test/ast_smt_pp.cpp +++ /dev/null @@ -1,90 +0,0 @@ -/*++ -Copyright (c) 2008 Microsoft Corporation - -Module Name: - - tst_ast_smt_pp.cpp - -Abstract: - - Test AST Pretty printing module - -Author: - - Nikolaj Bjorner (nbjorner) 2008-09-04 - -Revision History: - ---*/ -#include "ast.h" -#include "ast_smt_pp.h" -#include "smtparser.h" -#include -#include - -void tst_ast_smt_pp() -{ - ast_manager m; - smtlib::parser* parser = smtlib::parser::create(m); - - parser->initialize_smtlib(); - - - if (!parser->parse_string( - "(benchmark test :extrasorts (A B) :extrafuns ((f A A) (g A A A) (x A) (p A bool)) \n" - ":extrafuns ((arg0 BitVec[8]) (arg1 BitVec[8]) (arg2 BitVec[8]))\n" - ":formula (p (f x))\n" - ":extrafuns ((x1 Int) (y1 Int))\n" - ":formula (<= 1 (+ x1 y1))\n" - ":formula (let (x (g x x)) (let (x (g x x)) (let (x (g x x)) (let (x (g x x)) (p (g x x))))))\n" - ":formula (p x)\n" - ":formula (bvsge (bvadd arg0 arg2) (extract[7:0] bv3[32]))\n" - ":formula (forall (x Int) (y Int) (z Int) (and (<= 1 x) (<= x y))) \n" - ":formula (forall (x Int) (y Int) (z Int) (and (<= 2 (ite (<= z 1) x (* 2 x))) (<= x y)))\n" - ":formula (forall (x Int) (y Int) (and (<= 2 (ite (forall (z Int) (<= z 1)) x (* 2 x))) (<= x y)))\n" - ":formula (forall (x Int) (y Int) (and (<= 2 (ite (forall (z Int) (or (> x y) (<= z 1))) x (* 2 x))) (<= x y)))\n" - ":extrafuns ((a1 Array))\n" - ":formula (= x1 (select (store a1 y1 y1) x1))\n" - ":extrafuns ((a2 Array[32:8]))\n" - ":formula (= arg0 (select a2 bv0[32]))\n" - ":datatypes ((list (cons (car Int) (cdr list)) nil))\n" - ":extrafuns ((a list) (b list) (c list))\n" - ":formula (is_nil nil)\n" - ":datatypes ((list1 (cons1 (car1 Int) (cdr1 list2)) nil1) (list2 (cons1 (car2 list) (cdr2 list1)) nil2) )\n" - ":formula (is_nil2 nil2)\n" - ")")) { - SASSERT(false); - dealloc(parser); - return; - } - - smtlib::benchmark* b = parser->get_benchmark(); - - for (unsigned j = 0; j < b->get_num_formulas(); ++j) { - expr* e = b->begin_formulas()[j]; - ast_smt_pp pp(m); - pp.display(std::cout, e); - } - - - for (unsigned j = 0; j < b->get_num_formulas(); ++j) { - expr* e = b->begin_formulas()[j]; - - // print and parse formula again. - std::ostringstream buffer; - ast_smt_pp pp(m); - pp.display(buffer, e); - ast_manager m2; - smtlib::parser* parser2 = smtlib::parser::create(m2); - parser2->initialize_smtlib(); - if (!parser2->parse_string(buffer.str().c_str())) { - SASSERT(false); - dealloc(parser2); - return; - } - dealloc(parser2); - } - - - dealloc(parser); -} diff --git a/src/dead/test/ackermanize.cpp b/src/test/dead/ackermanize.cpp similarity index 100% rename from src/dead/test/ackermanize.cpp rename to src/test/dead/ackermanize.cpp diff --git a/src/dead/test/core_theory.cpp b/src/test/dead/core_theory.cpp similarity index 100% rename from src/dead/test/core_theory.cpp rename to src/test/dead/core_theory.cpp diff --git a/src/dead/test/dimacs.cpp b/src/test/dead/dimacs.cpp similarity index 100% rename from src/dead/test/dimacs.cpp rename to src/test/dead/dimacs.cpp diff --git a/src/dead/test/distinct.cpp b/src/test/dead/distinct.cpp similarity index 100% rename from src/dead/test/distinct.cpp rename to src/test/dead/distinct.cpp diff --git a/src/test/expr_context_simplifier.cpp b/src/test/dead/expr_context_simplifier.cpp similarity index 100% rename from src/test/expr_context_simplifier.cpp rename to src/test/dead/expr_context_simplifier.cpp diff --git a/src/dead/test/fingerprint.cpp b/src/test/dead/fingerprint.cpp similarity index 100% rename from src/dead/test/fingerprint.cpp rename to src/test/dead/fingerprint.cpp diff --git a/src/dead/test/gate.cpp b/src/test/dead/gate.cpp similarity index 100% rename from src/dead/test/gate.cpp rename to src/test/dead/gate.cpp diff --git a/src/dead/test/interval_arithmetic.cpp b/src/test/dead/interval_arithmetic.cpp similarity index 100% rename from src/dead/test/interval_arithmetic.cpp rename to src/test/dead/interval_arithmetic.cpp diff --git a/src/test/qe_defs.cpp b/src/test/dead/qe_defs.cpp similarity index 100% rename from src/test/qe_defs.cpp rename to src/test/dead/qe_defs.cpp diff --git a/src/test/quant_elim.cpp b/src/test/dead/quant_elim.cpp similarity index 100% rename from src/test/quant_elim.cpp rename to src/test/dead/quant_elim.cpp diff --git a/src/dead/test/relevancy.cpp b/src/test/dead/relevancy.cpp similarity index 100% rename from src/dead/test/relevancy.cpp rename to src/test/dead/relevancy.cpp diff --git a/src/dead/test/sat.cpp b/src/test/dead/sat.cpp similarity index 100% rename from src/dead/test/sat.cpp rename to src/test/dead/sat.cpp diff --git a/src/dead/test/simplex_polynomial.cpp b/src/test/dead/simplex_polynomial.cpp similarity index 100% rename from src/dead/test/simplex_polynomial.cpp rename to src/test/dead/simplex_polynomial.cpp diff --git a/src/test/symmetry.cpp b/src/test/dead/symmetry.cpp similarity index 100% rename from src/test/symmetry.cpp rename to src/test/dead/symmetry.cpp diff --git a/src/dead/test/template_models.cpp b/src/test/dead/template_models.cpp similarity index 100% rename from src/dead/test/template_models.cpp rename to src/test/dead/template_models.cpp diff --git a/src/dead/test/th_propagation.cpp b/src/test/dead/th_propagation.cpp similarity index 100% rename from src/dead/test/th_propagation.cpp rename to src/test/dead/th_propagation.cpp diff --git a/src/dead/test/trail.cpp b/src/test/dead/trail.cpp similarity index 100% rename from src/dead/test/trail.cpp rename to src/test/dead/trail.cpp diff --git a/src/dead/test/watch_list.cpp b/src/test/dead/watch_list.cpp similarity index 100% rename from src/dead/test/watch_list.cpp rename to src/test/dead/watch_list.cpp diff --git a/src/test/dl_rule_set.cpp b/src/test/dl_rule_set.cpp deleted file mode 100644 index d68bdc3c7..000000000 --- a/src/test/dl_rule_set.cpp +++ /dev/null @@ -1,118 +0,0 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - dl_rule_set.cpp - -Abstract: - - - -Author: - - Leonardo de Moura (leonardo) 2010-05-18. - -Revision History: - ---*/ -#include"dl_context.h" -#include"dl_rule_set.h" -#include"dl_mk_filter_rules.h" -#include"dl_mk_simple_joins.h" -#include"smtparser.h" -#include"ast_pp.h" -#include -#include - -void tst_dl_rule_set() { - enable_trace("mk_filter_rules"); - front_end_params params; - ast_manager m; - smtlib::parser * parser = smtlib::parser::create(m); - parser->initialize_smtlib(); - datalog::context ctx(m, params); - datalog::rule_set rs(ctx); - datalog::rule_manager& rm = ctx.get_rule_manager(); - datalog::rule_ref_vector rv(rm); - - - if (!parser->parse_string( - "(benchmark test\n" - ":extrapreds ((T Int Int) (Q Int Int) (R Int Int Int) (S Int Int Int) (DynActual Int Int Int) (GlobalSym Int Int) (HeapPointsTo Int Int Int) (Calls Int Int)) \n" - ":extrapreds ((Actual Int Int Int) (PointsTo Int Int) (PointsTo0 Int Int) (FuncDecl0 Int Int) (Assign Int Int) (Load Int Int Int))\n" - ":formula (forall (x Int) (=> (Q x 1) (T x x)))\n" - ":formula (forall (v Int) (h Int) (=> (PointsTo0 v h) (PointsTo v h)))\n" - ":formula (forall (v Int) (h Int) (=> (FuncDecl0 v h) (PointsTo v h)))\n" - ":formula (forall (v Int) (h Int) (=> (FuncDecl0 v h) (PointsTo v h)))\n" - ":formula (forall (v1 Int) (v2 Int) (h Int) (=> (and (PointsTo v2 h) (Assign v1 v2)) (PointsTo v1 h)))\n" - ":formula (forall (x Int) (y Int) (z Int) (=> (and (Q x y) (T y z)) (T x y)))\n" - ":formula (forall (i1 Int) (v Int) (fun Int) (c Int) (v1 Int) (h Int) (h1 Int) (=> (and (GlobalSym 0 fun) (HeapPointsTo fun 1 c) (Calls i1 c) (Actual i1 3 v1) (PointsTo v1 h) (HeapPointsTo h 0 h1) (PointsTo v h1)) (DynActual i1 2 v)))\n" - ":formula (forall (i1 Int) (v Int) (fun Int) (c Int) (v1 Int) (h Int) (h1 Int) (=> (and (GlobalSym 0 fun) (HeapPointsTo fun 1 c) (Calls i1 c) (Actual i1 3 v1) (PointsTo v1 h) (HeapPointsTo h 1 h1) (PointsTo v h1)) (DynActual i1 3 v)))\n" - ":formula (forall (i1 Int) (v Int) (fun Int) (c Int) (v1 Int) (h Int) (h1 Int) (=> (and (GlobalSym 0 fun) (HeapPointsTo fun 1 c) (Calls i1 c) (Actual i1 3 v1) (PointsTo v1 h) (HeapPointsTo h 2 h1) (PointsTo v h1)) (DynActual i1 4 v)))\n" - ":formula (forall (v1 Int) (v2 Int) (h1 Int) (h2 Int) (f Int) (=> (and (Load v2 v1 f) (PointsTo v1 h1) (HeapPointsTo h1 f h2)) (PointsTo v2 h1)))\n" - ":formula (forall (v1 Int) (v2 Int) (h1 Int) (h2 Int) (f Int) (=> (and (Load v2 v1 0) (HeapPointsTo h1 f h2)) (PointsTo v2 h1)))\n" - ":formula (forall (v1 Int) (v2 Int) (h1 Int) (h2 Int) (f Int) (=> (and (not (Load v2 v1 0)) (HeapPointsTo h1 f h2)) (PointsTo v2 h1)))\n" - ")")) { - SASSERT(false); - dealloc(parser); - return; - } - - smtlib::benchmark * b = parser->get_benchmark(); - - - for (unsigned j = 0; j < b->get_num_formulas(); ++j) { - expr * e = b->begin_formulas()[j]; - ptr_vector todo; - todo.push_back(e); - while (!todo.empty()) { - e = todo.back(); - todo.pop_back(); - if (is_quantifier(e)) { - e = to_quantifier(e)->get_expr(); - todo.push_back(e); - } - else if (is_app(e)) { - app* a = to_app(e); - if (is_uninterp(e) && !ctx.is_predicate(a->get_decl())) { - std::cout << "registering " << a->get_decl()->get_name() << "\n"; - - ctx.register_predicate(a->get_decl()); - } - else { - todo.append(a->get_num_args(), a->get_args()); - } - } - } - } - - - for (unsigned j = 0; j < b->get_num_formulas(); ++j) { - expr * e = b->begin_formulas()[j]; - if (is_quantifier(e)) { - try { - rm.mk_rule(e, rv); - } - catch(...) { - std::cerr << "ERROR: it is not a valid Datalog rule:\n" << mk_pp(e, m) << "\n"; - } - } - } - rs.add_rules(rv.size(), rv.c_ptr()); - rs.display(std::cout); - - datalog::mk_filter_rules p(ctx); - model_converter_ref mc; - proof_converter_ref pc; - datalog::rule_set * new_rs = p(rs, mc, pc); - std::cout << "\nAfter mk_filter:\n"; - new_rs->display(std::cout); - datalog::mk_simple_joins p2(ctx); - datalog::rule_set * new_rs2 = p2(*new_rs, mc, pc); - std::cout << "\nAfter mk_simple_joins:\n"; - new_rs2->display(std::cout); - dealloc(new_rs); - dealloc(new_rs2); - dealloc(parser); -} diff --git a/src/test/expr_delta.cpp b/src/test/expr_delta.cpp deleted file mode 100644 index fae80336d..000000000 --- a/src/test/expr_delta.cpp +++ /dev/null @@ -1,127 +0,0 @@ -#include "expr_delta.h" -#include "smtparser.h" -#include "ast_pp.h" -#include "ast_smt_pp.h" - -static void iterate_delta(ast_manager& m, expr_delta& delta) { - unsigned n = 0; - expr_ref_vector result(m); - std::cout << "Delta\n"; - while (true) { - result.reset(); - if (!delta.delta_dfs(n, result)) { - return; - } - std::cout << n << ": "; - for (unsigned i = 0; i < result.size(); ++i) { - std::cout << mk_pp(result[i].get(), m) << " "; - } - std::cout << "\n"; - n++; - } -} - -void tst_expr_delta1() { - ast_manager m; - smtlib::parser* parser = smtlib::parser::create(m); - parser->initialize_smtlib(); - - parser->parse_string( - "(benchmark samples :logic QF_LIA \n" - " :extrafuns ((a Int) (b Int) (c Int)) \n" - " :assumption (> a 0) \n" - " :assumption (> b 0) \n" - " :formula (forall (x Int) (y Int) (z Int) (and (<= 1 x) (<= x y))) \n" - " :formula (forall (x Int) (y Int) (z Int) (and (<= 2 (ite (<= z 1) x (* 2 x))) (<= x y)))\n" - " :formula (forall (x Int) (y Int) (and (<= 2 (ite (forall (z Int) (<= z 1)) x (* 2 x))) (<= x y)))\n" - " :formula (forall (x Int) (y Int) (and (<= 2 (ite (forall (z Int) (or (> x y) (<= z 1))) x (* 2 x))) (<= x y)))\n" - ")" - ); - - smtlib::benchmark* b = parser->get_benchmark(); - - for (unsigned j = 0; j < b->get_num_formulas(); ++j) { - expr_delta delta(m); - - for (unsigned i = 0; i < b->get_num_assumptions(); ++i) { - delta.assert_cnstr(b->get_assumptions()[i]); - } - delta.assert_cnstr(b->begin_formulas()[j]); - iterate_delta(m, delta); - } - - dealloc(parser); -} - -static void get_expr_delta(unsigned position, char const* in, char const* out) { - ast_manager m; - smtlib::parser* parser = smtlib::parser::create(m); - parser->initialize_smtlib(); - - if (!parser->parse_file(in)) { - std::cout << "error parsing file\n"; - dealloc(parser); - return; - } - - smtlib::benchmark* b = parser->get_benchmark(); - - SASSERT(b->get_num_formulas() == 1); - expr_delta delta(m); - - for (unsigned i = 0; i < b->get_num_assumptions(); ++i) { - delta.assert_cnstr(b->get_assumptions()[i]); - } - delta.assert_cnstr(b->begin_formulas()[0]); - - - expr_ref_vector result(m); - if (!delta.delta_dfs(position, result)) { - std::cout << "done\n"; - } - else { - ast_smt_pp pp(m); - std::ofstream outf(out); - if (outf.bad() || outf.fail()) { - std::cout << "Could not open output\n"; - } - else { - switch(b->get_status()) { - case smtlib::benchmark::UNKNOWN: - pp.set_status("unknown"); - break; - case smtlib::benchmark::SAT: - pp.set_status("sat"); - break; - case smtlib::benchmark::UNSAT: - pp.set_status("unsat"); - break; - } - pp.set_logic(b->get_logic().str().c_str()); - for (unsigned i = 0; i + 1 < result.size(); ++i) { - pp.add_assumption(result[i].get()); - } - pp.display(outf, result[result.size()-1].get()); - - std::cout << "ok\n"; - } - } - - dealloc(parser); -} - -void tst_expr_delta(char** argv, int argc, int& i) { - if (i + 3 >= argc) { - std::cout << "Usage: \n"; - return; - } - ++i; - unsigned position = atol(argv[i]); - ++i; - char const* in_file = argv[i]; - ++i; - char const* out_file = argv[i]; - - get_expr_delta(position, in_file, out_file); - -} diff --git a/src/test/expr_pattern_match.cpp b/src/test/expr_pattern_match.cpp deleted file mode 100644 index e7088913e..000000000 --- a/src/test/expr_pattern_match.cpp +++ /dev/null @@ -1,51 +0,0 @@ -#include "expr_pattern_match.h" -#include "smtparser.h" -#include "ast_pp.h" -#include "arith_decl_plugin.h" -#include "bv_decl_plugin.h" -#include "array_decl_plugin.h" -#include "reg_decl_plugins.h" - -void tst_expr_pattern_match() { - ast_manager manager; - reg_decl_plugins(manager); - - expr_pattern_match apm(manager); - - apm.display(std::cout); - - const char* test_string = "(benchmark patterns :status unknown :logic ALL \n" - ":extrasorts (S) \n" - ":extrafuns ((R S S bool)) \n" - ":formula (forall (x S) (y S) (z S) \n" - " (or (not (R x y)) (not (R y z)) (R x z)) \n" - " ; :pats { (R x y) (R y z) } \n" - " :weight { 2 } \n" - " )\n" - ")"; - smtlib::parser* parser = smtlib::parser::create(manager); - parser->initialize_smtlib(); - std::cout << "parsing test string\n"; - if (!parser->parse_string(test_string)) { - UNREACHABLE(); - } - std::cout << "test string parsed\n"; - smtlib::benchmark* bench = parser->get_benchmark(); - - for (unsigned i = 0; i < bench->get_num_formulas(); ++i) { - expr* fml = bench->begin_formulas()[i]; - SASSERT(fml->get_kind() == AST_QUANTIFIER); - quantifier* qf = to_quantifier(fml); - app_ref_vector patterns(manager); - unsigned weight = 0; - if (apm.match_quantifier(qf, patterns, weight)) { - std::cout << "Found pattern match\n"; - for (unsigned i = 0; i < patterns.size(); ++i) { - ast_pp(std::cout, patterns[i].get(), manager) << "\n"; - } - std::cout << "weight: " << weight << "\n"; - } - } - dealloc(parser); - -} diff --git a/src/test/grobner.cpp b/src/test/grobner.cpp deleted file mode 100644 index 89aea5049..000000000 --- a/src/test/grobner.cpp +++ /dev/null @@ -1,94 +0,0 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - grobner.cpp - -Abstract: - - - -Author: - - Leonardo de Moura (leonardo) 2008-12-05. - -Revision History: - ---*/ -#include"smtparser.h" -#include"ast_pp.h" -#include"arith_decl_plugin.h" -#include"simplifier.h" -#include"basic_simplifier_plugin.h" -#include"arith_simplifier_plugin.h" -#include"front_end_params.h" -#include"grobner.h" -#include"reg_decl_plugins.h" - -void display_eqs(grobner & gb, v_dependency_manager & dep_m) { - std::cerr << "RESULT:\n"; - ptr_vector eqs; - gb.get_equations(eqs); - ptr_vector::iterator it = eqs.begin(); - ptr_vector::iterator end = eqs.end(); - for (; it != end; ++it) { - grobner::equation * eq = *it; - ptr_vector exs; - v_dependency * d = eq->get_dependency(); - dep_m.linearize(d, exs); - std::cerr << "{"; - ptr_vector::iterator it2 = exs.begin(); - ptr_vector::iterator end2 = exs.end(); - for (bool first = true; it2 != end2; ++it2) { - if (first) first = false; else std::cerr << " "; - std::cerr << *it2; - } - std::cerr << "}, lc: " << eq->is_linear_combination() << ", "; - gb.display_equation(std::cerr, *eq); - } -} - -void tst_grobner(char ** argv, int argc, int & i) { - front_end_params params; - if (i + 1 < argc) { - char const* file_path = argv[i+1]; - - ast_manager m; - smtlib::parser* parser = smtlib::parser::create(m); - reg_decl_plugins(m); - parser->initialize_smtlib(); - - if (!parser->parse_file(file_path)) { - std::cout << "Could not parse file : " << file_path << std::endl; - dealloc(parser); - return; - } - - smtlib::benchmark* b = parser->get_benchmark(); - simplifier simp(m); - basic_simplifier_plugin * bp = alloc(basic_simplifier_plugin, m); - simp.register_plugin(bp); - simp.register_plugin(alloc(arith_simplifier_plugin, m, *bp, params)); - arith_util util(m); - v_dependency_manager dep_m; - grobner gb(m, dep_m); - - ptr_vector::const_iterator it = b->begin_axioms(); - ptr_vector::const_iterator end = b->end_axioms(); - for (unsigned idx = 1; it != end; ++it, ++idx) { - expr * ax = *it; - expr_ref s_ax(m); - proof_ref pr(m); - simp(ax, s_ax, pr); - std::cerr << mk_pp(s_ax, m) << "\n"; - if (m.is_eq(s_ax)) - gb.assert_eq(s_ax, dep_m.mk_leaf(reinterpret_cast(idx))); - } - gb.display(std::cerr); - gb.compute_basis(1024); - display_eqs(gb, dep_m); - dealloc(parser); - } -} - diff --git a/src/test/main.cpp b/src/test/main.cpp index e99e96729..acbea0761 100644 --- a/src/test/main.cpp +++ b/src/test/main.cpp @@ -123,7 +123,6 @@ int main(int argc, char ** argv) { memory::initialize(0); bool do_display_usage = false; parse_cmd_line_args(argc, argv, do_display_usage); - TST_ARGV(grobner); TST(random); TST(vector); TST(symbol_table); @@ -131,23 +130,17 @@ int main(int argc, char ** argv) { TST(symbol); TST(heap); TST(hashtable); - TST_ARGV(smtparser); TST(rational); TST(inf_rational); TST(ast); TST(optional); TST(bit_vector); - TST(ast_pp); - TST(ast_smt_pp); - TST_ARGV(expr_delta); TST(string_buffer); TST(map); TST(diff_logic); TST(uint_set); TST_ARGV(expr_rand); - TST(expr_context_simplifier); TST(ini_file); - TST(expr_pattern_match); TST(list); TST(small_object_allocator); TST(timeout); @@ -157,9 +150,6 @@ int main(int argc, char ** argv) { TST(bit_blaster); TST(var_subst); TST(simple_parser); - TST(symmetry); - TST_ARGV(symmetry_parse); - TST_ARGV(symmetry_prove); TST(api); TST(old_interval); TST(interval_skip_list); @@ -167,10 +157,8 @@ int main(int argc, char ** argv) { TST(memory); TST(get_implied_equalities); TST(arith_simplifier_plugin); - TST(quant_elim); TST(matcher); TST(datalog_parser); - TST(dl_rule_set); TST_ARGV(datalog_parser_file); TST(object_allocator); TST(mpz); @@ -208,7 +196,6 @@ int main(int argc, char ** argv) { TST(prime_generator); TST(permutation); TST(nlsat); - TST(qe_defs); TST(ext_numeral); TST(interval); TST(quant_solve); diff --git a/src/test/smtparser.cpp b/src/test/smtparser.cpp deleted file mode 100644 index dc4f0eb74..000000000 --- a/src/test/smtparser.cpp +++ /dev/null @@ -1,52 +0,0 @@ -#ifdef _WINDOWS -#include -#include -#include -#include -#include "smtparser.h" -#include "for_each_file.h" -#include "array_decl_plugin.h" -#include "bv_decl_plugin.h" -#include "reg_decl_plugins.h" - -class for_each_file_smt : public for_each_file_proc { -public: - for_each_file_smt() {} - - bool operator()(char const * file_path) { - bool result = true; - std::cout << "Parsing: " << file_path << std::endl; - - ast_manager ast_manager; - smtlib::parser* parser = smtlib::parser::create(ast_manager); - reg_decl_plugins(ast_manager); - - parser->initialize_smtlib(); - - if (!parser->parse_file(file_path)) { - std::cout << "Could not parse file : " << file_path << std::endl; - result = false; - } - dealloc(parser); - return result; - } -}; - - -static bool test_directory(char const * base) { - for_each_file_smt foreach; - return for_each_file(foreach, base, "*.smt"); -} - -void tst_smtparser(char** argv, int argc, int & i) { - bool result = true; - if (i + 1 < argc) { - result = test_directory(argv[i+1]); - i += 1; - } - SASSERT(result); -} -#else -void tst_smtparser(char** argv, int argc, int & i) { -} -#endif diff --git a/src/test/var_subst.cpp b/src/test/var_subst.cpp index efc4555fe..3e75d1527 100644 --- a/src/test/var_subst.cpp +++ b/src/test/var_subst.cpp @@ -17,7 +17,6 @@ Revision History: --*/ #include"var_subst.h" -#include"smtparser.h" #include"ast_pp.h" #include"arith_decl_plugin.h" #include"bv_decl_plugin.h" @@ -104,22 +103,4 @@ void tst_var_subst() { ast_manager m; reg_decl_plugins(m); tst_subst(m); - - scoped_ptr parser = smtlib::parser::create(m); - parser->initialize_smtlib(); - - parser->parse_string( - "(benchmark samples :logic AUFLIA\n" - " :extrafuns ((f Int Int) (g Int Int Int) (a Int) (b Int))\n" - " :formula (forall (x Int) (or (= (f x) x) (forall (y Int) (z Int) (= (g x y) (f z)))))\n" - " :formula (forall (x Int) (w Int) (or (= (f x) x) (forall (y Int) (z Int) (or (= (g x y) (g w z)) (forall (x1 Int) (= (f x1) (g x y)))))))\n" - ")" - ); - - smtlib::benchmark* b = parser->get_benchmark(); - - smtlib::theory::expr_iterator it = b->begin_formulas(); - smtlib::theory::expr_iterator end = b->end_formulas(); - for (; it != end; ++it) - tst_instantiate(m, *it); }