mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

test horner

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-07-11 12:43:47 -07:00
parent 8e21342549
commit ad9ecad73c
3 changed files with 47 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/math/lp/horner.h
View file

@ -28,9 +28,9 @@ class core;
class horner : common {
typedef nla_expr<rational> nex;
intervals m_intervals;
public:
typedef nla_expr<rational> nex;
horner(core *core);
void horner_lemmas();

35
src/math/lp/nla_expr.h
View file

@ -17,6 +17,7 @@ Revision History:
--*/
#pragma once
#include <initializer_list>
#include "math/lp/nla_defs.h"
namespace nla {
enum class expr_type { SUM, MUL, VAR, SCALAR, UNDEF };
@ -157,21 +158,33 @@ public:
m_children.push_back(e);
}
static nla_expr sum(const nla_expr& v, const nla_expr & w) {
nla_expr r(expr_type::SUM);
r.add_child(v);
r.add_child(w);
return r;
void add_child(const T& k) {
m_children.push_back(scalar(k));
}
static nla_expr mul(const nla_expr& v, const nla_expr & w) {
nla_expr r(expr_type::MUL);
r.add_child(v);
r.add_child(w);
void add_children() { }
template <typename K, typename ...Args>
void add_children(K e, Args ... es) {
add_child(e);
add_children(es ...);
}
template <typename K, typename ... Args>
static nla_expr sum(K e, Args ... es) {
nla_expr r(expr_type::SUM);
r.add_children(e, es...);
return r;
}
static nla_expr mul(const T& v, const nla_expr & w) {
template <typename K, typename ... Args>
static nla_expr mul(K e, Args ... es) {
nla_expr r(expr_type::MUL);
r.add_children(e, es...);
return r;
}
static nla_expr mul(const T& v, nla_expr & w) {
if (v == 1)
return w;
nla_expr r(expr_type::MUL);

23
src/test/lp/lp.cpp
View file

@ -55,6 +55,7 @@
#include "math/lp/general_matrix.h"
#include "math/lp/lp_bound_propagator.h"
#include "math/lp/nla_solver.h"
#include "math/lp/horner.h"
namespace nla {
void test_order_lemma();
void test_monotone_lemma();
@ -64,6 +65,17 @@ void test_basic_lemma_for_mon_zero_from_monomial_to_factors();
void test_basic_lemma_for_mon_zero_from_factors_to_monomial();
void test_basic_lemma_for_mon_neutral_from_monomial_to_factors();
void test_basic_lemma_for_mon_neutral_from_factors_to_monomial();
void test_cn() {
typedef horner::nex nex;
enable_trace("nla_cn");
nex a = nex::var(0), b = nex::var(1), c = nex::var(2), d = nex::var(3), e = nex::var(4);
nex aad = nex::mul(a, a, d);
}
}
namespace lp {
@ -71,7 +83,7 @@ unsigned seed = 1;
class my_bound_propagator : public lp_bound_propagator {
public:
my_bound_propagator(lar_solver & ls): lp_bound_propagator(ls, nullptr) {}
my_bound_propagator(lar_solver & ls): lp_bound_propagator(ls) {}
void consume(mpq const& v, lp::constraint_index j) override {}
};
@ -1907,6 +1919,7 @@ void test_replace_column() {
void setup_args_parser(argument_parser & parser) {
parser.add_option_with_help_string("-nla_cn", "test cross nornmal form");
parser.add_option_with_help_string("-nla_blfmz_mf", "test_basic_lemma_for_mon_zero_from_factor_to_monomial");
parser.add_option_with_help_string("-nla_blfmz_fm", "test_basic_lemma_for_mon_zero_from_monomials_to_factor");
parser.add_option_with_help_string("-nla_order", "test nla_solver order lemma");
@ -3570,6 +3583,7 @@ void test_nla_order_lemma() {
nla::test_order_lemma();
}
void test_lp_local(int argn, char**argv) {
// initialize_util_module();
@ -3586,6 +3600,13 @@ void test_lp_local(int argn, char**argv) {
args_parser.print();
if (args_parser.option_is_used("-nla_cn")) {
#ifdef Z3DEBUG
nla::test_cn();
#endif
return finalize(0);
}
if (args_parser.option_is_used("-nla_order")) {
#ifdef Z3DEBUG
test_nla_order_lemma();