mirror of
https://github.com/Z3Prover/z3
synced 2025-08-10 05:00:51 +00:00
* introduce int_solver.h Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * add int_solver class Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * track which var is an integer Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * add queries for integrality of vars Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * resurrect lp_tst in its own director lp Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * add file Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * add_constraint has got a body Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * fix add_constraint and substitute_terms_in_linear_expression Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * after merge with Z3Prover Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * adding stub check_int_feasibility() Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * Dev (#50) * initial skeletons for nra solver Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * initial skeletons for nra solver Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * small fix in lar_solver.cpp Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * adding some content to the new check_int_feasibility() Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * Dev (#51) * initial skeletons for nra solver Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * initial skeletons for nra solver Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * adding more nlsat Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * nlsat integration Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * adding constraints Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * adding nra solver Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add missing initialization Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * adding nra solver Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * test Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * Dev (#53) * change in a comment Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * Disabled debug output * removing FOCI2 interface from interp * remove foci reference from cmakelist.txt Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * initial skeletons for nra solver Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * initial skeletons for nra solver Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * adding more nlsat Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * nlsat integration Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * adding constraints Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * adding nra solver Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add missing initialization Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * adding nra solver Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * adding nra Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * debugging nra Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * updates to nra_solver integration to call it directly from theory_lra instead of over lar_solver Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * n/a Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * integrate nlsat Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * tidy Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * preserve is_int flag Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * remove a debug printout Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * Dev (#54) * change in a comment Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * Disabled debug output * removing FOCI2 interface from interp * remove foci reference from cmakelist.txt Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * initial skeletons for nra solver Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * initial skeletons for nra solver Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * adding more nlsat Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * nlsat integration Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * adding constraints Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * adding nra solver Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add missing initialization Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * adding nra solver Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * adding nra Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * debugging nra Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * updates to nra_solver integration to call it directly from theory_lra instead of over lar_solver Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * n/a Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * integrate nlsat Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * tidy Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * use integer test from lra solver, updated it to work on term variables Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix equality check in assume-eq Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix model_is_int_feasible Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * untested gcd_test() Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * call fill_explanation_from_fixed_columns() Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * add the call to pivot_fixed_vars_from_basis() to int_solver.cpp::check() Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * port more of theory_arith_int.h Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * use statistics of lar_solver by theory_lra.cpp Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * port more code to int_solver.cpp Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * add an assert Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * more int porting Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * fix a bug in pivot_fixed_vars_from_basis Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * small change Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * implement find_inf_int_base_column() Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * catch unregistered vars in add_var_bound Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * add a file Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * compile for vs2012 Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * fix asserts in add_var_bound Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * fix the lp_solver init when workig on an mps file Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * towards int_solver::check() Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * change in int_solver::check() signature Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * add handlers for lia moves Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * spacing Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
87 lines
1.7 KiB
C++
87 lines
1.7 KiB
C++
/*++
|
|
Copyright (c) 2017 Microsoft Corporation
|
|
|
|
Module Name:
|
|
|
|
<name>
|
|
|
|
Abstract:
|
|
|
|
<abstract>
|
|
|
|
Author:
|
|
|
|
Lev Nachmanson (levnach)
|
|
|
|
Revision History:
|
|
|
|
|
|
--*/
|
|
|
|
#pragma once
|
|
|
|
// reads a text file
|
|
#include <string>
|
|
#include <vector>
|
|
#include <unordered_map>
|
|
#include <iostream>
|
|
#include <fstream>
|
|
#include "util/lp/lp_utils.h"
|
|
#include "util/lp/lp_solver.h"
|
|
|
|
namespace lp {
|
|
|
|
template <typename T>
|
|
struct test_result {
|
|
lp_status m_status;
|
|
T m_cost;
|
|
std::unordered_map<std::string, T> column_values;
|
|
};
|
|
|
|
template <typename T>
|
|
class test_file_reader {
|
|
struct raw_blob {
|
|
std::vector<std::string> m_unparsed_strings;
|
|
std::vector<raw_blob> m_blobs;
|
|
};
|
|
|
|
struct test_file_blob {
|
|
std::string m_name;
|
|
std::string m_content;
|
|
std::unordered_map<std::string, std::string> m_table;
|
|
std::unordered_map<std::string, test_file_blob> m_blobs;
|
|
|
|
test_result<T> * get_test_result() {
|
|
test_result<T> * tr = new test_result<T>();
|
|
throw "not impl";
|
|
return tr;
|
|
}
|
|
};
|
|
std::ifstream m_file_stream;
|
|
public:
|
|
// constructor
|
|
test_file_reader(std::string file_name) : m_file_stream(file_name) {
|
|
if (!m_file_stream.is_open()) {
|
|
std::cout << "cannot open file " << "\'" << file_name << "\'" << std::endl;
|
|
}
|
|
}
|
|
|
|
raw_blob scan_to_row_blob() {
|
|
}
|
|
|
|
test_file_blob scan_row_blob_to_test_file_blob(raw_blob /* rblob */) {
|
|
}
|
|
|
|
test_result<T> * get_test_result() {
|
|
if (!m_file_stream.is_open()) {
|
|
return nullptr;
|
|
}
|
|
|
|
raw_blob rblob = scan_to_row_blob();
|
|
|
|
test_file_blob tblob = scan_row_blob_to_test_file_blob(rblob);
|
|
|
|
return tblob.get_test_result();
|
|
}
|
|
};
|
|
}
|