mirror of
https://github.com/Z3Prover/z3
synced 2025-10-10 17:58:06 +00:00
rename the files
Signed-off-by: Lev <levnach@hotmail.com>
This commit is contained in:
parent
103808094a
commit
56ae577c97
4 changed files with 3 additions and 3 deletions
49
src/util/lp/nla_solver.h
Normal file
49
src/util/lp/nla_solver.h
Normal file
|
@ -0,0 +1,49 @@
|
|||
/*++
|
||||
Copyright (c) 2017 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
<name>
|
||||
|
||||
Abstract:
|
||||
|
||||
<abstract>
|
||||
|
||||
Author:
|
||||
Nikolaj Bjorner (nbjorner)
|
||||
Lev Nachmanson (levnach)
|
||||
|
||||
Revision History:
|
||||
|
||||
|
||||
--*/
|
||||
#pragma once
|
||||
#include "util/vector.h"
|
||||
#include "util/lp/lp_settings.h"
|
||||
#include "util/rlimit.h"
|
||||
#include "util/params.h"
|
||||
#include "nlsat/nlsat_solver.h"
|
||||
#include "util/lp/lar_solver.h"
|
||||
namespace niil {
|
||||
struct ineq {
|
||||
lp::lconstraint_kind m_cmp;
|
||||
lp::lar_term m_term;
|
||||
ineq(lp::lconstraint_kind cmp, const lp::lar_term& term) : m_cmp(cmp), m_term(term) {}
|
||||
};
|
||||
|
||||
typedef vector<ineq> lemma;
|
||||
|
||||
// nonlinear integer incremental linear solver
|
||||
class solver {
|
||||
struct imp;
|
||||
imp* m_imp;
|
||||
public:
|
||||
void add_monomial(lp::var_index v, unsigned sz, lp::var_index const* vs);
|
||||
solver(lp::lar_solver& s, reslimit& lim, params_ref const& p);
|
||||
~solver();
|
||||
void push();
|
||||
void pop(unsigned scopes);
|
||||
bool need_check();
|
||||
lbool check(lp::explanation&, lemma&);
|
||||
};
|
||||
}
|
Loading…
Add table
Add a link
Reference in a new issue