mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

resurrect lp_tst in its own director lp

Browse source 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
This commit is contained in:
Lev Nachmanson 2017-05-17 11:01:04 -07:00
parent d5e06303ef
commit 9a58eb63cb
8 changed files with 39 additions and 30 deletions
Download patch file Download diff file Expand all files Collapse all files

3
contrib/cmake/src/test/CMakeLists.txt
View file

@ -1,4 +1,5 @@
add_subdirectory(fuzzing)
add_subdirectory(lp)
################################################################################
# z3-test executable
################################################################################
@ -117,7 +118,7 @@ add_executable(test-z3
upolynomial.cpp
var_subst.cpp
vector.cpp
lp.cpp
lp/lp.cpp
${z3_test_extra_object_files}
)
z3_add_install_tactic_rule(${z3_test_deps})

6
contrib/cmake/src/test/lp/CMakeLists.txt Normal file
View file

@ -0,0 +1,6 @@
add_executable(lp_tst lp_main.cpp lp.cpp $<TARGET_OBJECTS:util> $<TARGET_OBJECTS:lp>)
target_compile_definitions(lp_tst PRIVATE ${Z3_COMPONENT_CXX_DEFINES})
target_compile_options(lp_tst PRIVATE ${Z3_COMPONENT_CXX_FLAGS})
target_include_directories(lp_tst PRIVATE ${Z3_COMPONENT_EXTRA_INCLUDE_DIRS})
target_link_libraries(lp_tst PRIVATE ${Z3_DEPENDENT_LIBS})
z3_append_linker_flag_list_to_target(lp_tst ${Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS})

0
src/test/argument_parser.h → src/test/lp/argument_parser.h
View file

44
src/test/lp.cpp → src/test/lp/lp.cpp
View file

@ -2691,8 +2691,8 @@ void test_term() {
lar_solver solver;
unsigned _x = 0;
unsigned _y = 1;
var_index x = solver.add_var(_x);
var_index y = solver.add_var(_y);
var_index x = solver.add_var(_x, false);
var_index y = solver.add_var(_y, false);
vector<std::pair<mpq, var_index>> term_ls;
term_ls.push_back(std::pair<mpq, var_index>((int)1, x));
@ -2719,8 +2719,8 @@ void test_term() {
void test_evidence_for_total_inf_simple(argument_parser & args_parser) {
lar_solver solver;
var_index x = solver.add_var(0);
var_index y = solver.add_var(1);
var_index x = solver.add_var(0, false);
var_index y = solver.add_var(1, false);
solver.add_var_bound(x, LE, -mpq(1));
solver.add_var_bound(y, GE, mpq(0));
vector<std::pair<mpq, var_index>> ls;
@ -2754,9 +2754,9 @@ If b becomes basic variable, then it is likely the old solver ends up with a row
return true;
};
lar_solver ls;
unsigned a = ls.add_var(0);
unsigned b = ls.add_var(1);
unsigned c = ls.add_var(2);
unsigned a = ls.add_var(0, false);
unsigned b = ls.add_var(1, false);
unsigned c = ls.add_var(2, false);
vector<std::pair<mpq, var_index>> coeffs;
coeffs.push_back(std::pair<mpq, var_index>(1, a));
coeffs.push_back(std::pair<mpq, var_index>(-1, c));
@ -2819,8 +2819,8 @@ If x9 becomes basic variable, then it is likely the old solver ends up with a ro
}
void test_bound_propagation_one_row() {
lar_solver ls;
unsigned x0 = ls.add_var(0);
unsigned x1 = ls.add_var(1);
unsigned x0 = ls.add_var(0, false);
unsigned x1 = ls.add_var(1, false);
vector<std::pair<mpq, var_index>> c;
c.push_back(std::pair<mpq, var_index>(1, x0));
c.push_back(std::pair<mpq, var_index>(-1, x1));
@ -2833,8 +2833,8 @@ void test_bound_propagation_one_row() {
}
void test_bound_propagation_one_row_with_bounded_vars() {
lar_solver ls;
unsigned x0 = ls.add_var(0);
unsigned x1 = ls.add_var(1);
unsigned x0 = ls.add_var(0, false);
unsigned x1 = ls.add_var(1, false);
vector<std::pair<mpq, var_index>> c;
c.push_back(std::pair<mpq, var_index>(1, x0));
c.push_back(std::pair<mpq, var_index>(-1, x1));
@ -2849,8 +2849,8 @@ void test_bound_propagation_one_row_with_bounded_vars() {
}
void test_bound_propagation_one_row_mixed() {
lar_solver ls;
unsigned x0 = ls.add_var(0);
unsigned x1 = ls.add_var(1);
unsigned x0 = ls.add_var(0, false);
unsigned x1 = ls.add_var(1, false);
vector<std::pair<mpq, var_index>> c;
c.push_back(std::pair<mpq, var_index>(1, x0));
c.push_back(std::pair<mpq, var_index>(-1, x1));
@ -2864,9 +2864,9 @@ void test_bound_propagation_one_row_mixed() {
void test_bound_propagation_two_rows() {
lar_solver ls;
unsigned x = ls.add_var(0);
unsigned y = ls.add_var(1);
unsigned z = ls.add_var(2);
unsigned x = ls.add_var(0, false);
unsigned y = ls.add_var(1, false);
unsigned z = ls.add_var(2, false);
vector<std::pair<mpq, var_index>> c;
c.push_back(std::pair<mpq, var_index>(1, x));
c.push_back(std::pair<mpq, var_index>(2, y));
@ -2888,9 +2888,9 @@ void test_bound_propagation_two_rows() {
void test_total_case_u() {
std::cout << "test_total_case_u\n";
lar_solver ls;
unsigned x = ls.add_var(0);
unsigned y = ls.add_var(1);
unsigned z = ls.add_var(2);
unsigned x = ls.add_var(0, false);
unsigned y = ls.add_var(1, false);
unsigned z = ls.add_var(2, false);
vector<std::pair<mpq, var_index>> c;
c.push_back(std::pair<mpq, var_index>(1, x));
c.push_back(std::pair<mpq, var_index>(2, y));
@ -2914,9 +2914,9 @@ bool contains_j_kind(unsigned j, lconstraint_kind kind, const mpq & rs, const ve
void test_total_case_l(){
std::cout << "test_total_case_l\n";
lar_solver ls;
unsigned x = ls.add_var(0);
unsigned y = ls.add_var(1);
unsigned z = ls.add_var(2);
unsigned x = ls.add_var(0, false);
unsigned y = ls.add_var(1, false);
unsigned z = ls.add_var(2, false);
vector<std::pair<mpq, var_index>> c;
c.push_back(std::pair<mpq, var_index>(1, x));
c.push_back(std::pair<mpq, var_index>(2, y));

2
src/test/smt_reader.h → src/test/lp/smt_reader.h
View file

@ -376,7 +376,7 @@ namespace lean {
void add_constraint_to_solver(lar_solver * solver, formula_constraint & fc) {
vector<std::pair<mpq, var_index>> ls;
for (auto & it : fc.m_coeffs) {
ls.push_back(std::make_pair(it.first, solver->add_var(register_name(it.second))));
ls.push_back(std::make_pair(it.first, solver->add_var(register_name(it.second), false)));
}
solver->add_constraint(ls, fc.m_kind, fc.m_right_side);
}

0
src/test/test_file_reader.h → src/test/lp/test_file_reader.h
View file

4
src/util/lp/init_lar_solver.cpp
View file

@ -2,8 +2,10 @@
Copyright (c) 2017 Microsoft Corporation
Author: Lev Nachmanson
*/
#include "util/lp/lar_solver.h"
// this file represents the intiialization functionality of lar_solver
#include "util/lp/lar_solver.h"
namespace lean {
bool lar_solver::strategy_is_undecided() const {

10
src/util/lp/mps_reader.h
View file

@ -810,7 +810,7 @@ public:
auto kind = get_lar_relation_from_row(row->m_type);
vector<std::pair<mpq, var_index>> ls;
for (auto s : row->m_row_columns) {
var_index i = solver->add_var(get_var_index(s.first));
var_index i = solver->add_var(get_var_index(s.first), false);
ls.push_back(std::make_pair(s.second, i));
}
solver->add_constraint(ls, kind, row->m_right_side);
@ -828,20 +828,20 @@ public:
void create_low_constraint_for_var(column* col, bound * b, lar_solver *solver) {
vector<std::pair<mpq, var_index>> ls;
var_index i = solver->add_var(col->m_index);
var_index i = solver->add_var(col->m_index, false);
ls.push_back(std::make_pair(numeric_traits<T>::one(), i));
solver->add_constraint(ls, GE, b->m_low);
}
void create_upper_constraint_for_var(column* col, bound * b, lar_solver *solver) {
var_index i = solver->add_var(col->m_index);
var_index i = solver->add_var(col->m_index, false);
vector<std::pair<mpq, var_index>> ls;
ls.push_back(std::make_pair(numeric_traits<T>::one(), i));
solver->add_constraint(ls, LE, b->m_upper);
}
void create_equality_contraint_for_var(column* col, bound * b, lar_solver *solver) {
var_index i = solver->add_var(col->m_index);
var_index i = solver->add_var(col->m_index, false);
vector<std::pair<mpq, var_index>> ls;
ls.push_back(std::make_pair(numeric_traits<T>::one(), i));
solver->add_constraint(ls, EQ, b->m_fixed_value);
@ -850,7 +850,7 @@ public:
void fill_lar_solver_on_columns(lar_solver * solver) {
for (auto s : m_columns) {
mps_reader::column * col = s.second;
solver->add_var(col->m_index);
solver->add_var(col->m_index, false);
auto b = col->m_bound;
if (b == nullptr) return;