mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 10:52:02 +00:00
Code Activity

initial skeletons for nra solver

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-05-23 16:12:46 -07:00
parent 1f425824ff
commit f1ca1de408
3 changed files with 80 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

31
src/util/lp/nra_solver.cpp Normal file
View file

@ -0,0 +1,31 @@
/*
Copyright (c) 2017 Microsoft Corporation
Author: Lev Nachmanson
*/
#pragma once
#include "util/lp/nra_solver.h"
namespace lp {
struct nra_solver::imp {
lean::lar_solver& s;
imp(lean::lar_solver& s): s(s) {}
lean::final_check_status check_feasible() {
return lean::final_check_status::GIVEUP;
}
};
nra_solver::nra_solver(lean::lar_solver& s) {
m_imp = alloc(imp, s);
}
nra_solver::~nra_solver() {
dealloc(m_imp);
}
lean::final_check_status nra_solver::check_feasible() {
return m_imp->check_feasible();
}
}