Skip to content

Commit

Permalink
Introduce symbolic simplification level (now tests OK)
Browse files Browse the repository at this point in the history
  • Loading branch information
gchabert committed Sep 8, 2020
1 parent fea6334 commit 4288495
Show file tree
Hide file tree
Showing 11 changed files with 60 additions and 35 deletions.
4 changes: 2 additions & 2 deletions src/system/ibex_ExtendedSystem.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,8 +17,8 @@ const char* ExtendedSystem::goal_name() {
return _goal_name;
}

ExtendedSystem::ExtendedSystem(const System& sys, double eps) :
NormalizedSystem(sys,eps,true) {
ExtendedSystem::ExtendedSystem(const System& sys, double eps, int simpl_level) :
NormalizedSystem(sys, eps, true, simpl_level) {
}

void ExtendedSystem::write_ext_box(const IntervalVector& box, IntervalVector& ext_box) const {
Expand Down
2 changes: 1 addition & 1 deletion src/system/ibex_ExtendedSystem.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -44,7 +44,7 @@ class ExtendedSystem : public NormalizedSystem {
*
* The goal of the extended system is "y".
*/
explicit ExtendedSystem(const System& sys, double eps=0);
explicit ExtendedSystem(const System& sys, double eps=0, int simpl_level=ExprNode::default_simpl_level);

/**
* \brief Name of the goal variable ("y").
Expand Down
13 changes: 7 additions & 6 deletions src/system/ibex_NormalizedSystem.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -57,7 +57,7 @@ CmpOp norm(CmpOp op) {

} // end namespace

NormalizedSystem::NormalizedSystem(const System& sys, double eps, bool extended) : original_sys_id(sys.id) {
NormalizedSystem::NormalizedSystem(const System& sys, double eps, bool extended, int simpl_level) : original_sys_id(sys.id) {

int nb_arg;
int k=0; // index of components of sys.f_ctrs
Expand Down Expand Up @@ -155,9 +155,9 @@ NormalizedSystem::NormalizedSystem(const System& sys, double eps, bool extended)

set_lb_ub(rhs, l, u, eps);

// simplification level 1 is enough for constant simplification
const ExprNode& ctrl = ((*fu)-ExprConstant::new_(u)).simplify(ExprNode::default_simpl_level);
const ExprNode& ctru = (ExprConstant::new_(l)-(*fl)).simplify(ExprNode::default_simpl_level);
// TODO: is running the full simplification process really necessary for just adding a constant?
const ExprNode& ctrl = ((*fu)-ExprConstant::new_(u)).simplify(simpl_level);
const ExprNode& ctru = (ExprConstant::new_(l)-(*fl)).simplify(simpl_level);
_ctrs.push_back(new NumConstraint(argsl,ExprCtr(ctrl,LEQ)));
_ctrs.push_back(new NumConstraint(argsu,ExprCtr(ctru,LEQ)));

Expand All @@ -177,7 +177,7 @@ NormalizedSystem::NormalizedSystem(const System& sys, double eps, bool extended)
const ExprNode* _fc=&ExprCopy().copy(fc.args(), argsc, fc.expr());

if (opc==GT || opc==GEQ) {
_fc = & (- (*_fc)).simplify(ExprNode::default_simpl_level); // reverse the inequality
_fc = & (- (*_fc)).simplify(simpl_level); // reverse the inequality
}

_ctrs.push_back(new NumConstraint(argsc,ExprCtr(*_fc,norm(opc))));
Expand Down Expand Up @@ -215,7 +215,8 @@ NormalizedSystem::NormalizedSystem(const System& sys, double eps, bool extended)
}

if (m>0) {
f_ctrs.init(args, ExprVector::new_col(Array<const ExprNode>(_f_ctr)).simplify(ExprNode::default_simpl_level));
//TODO: does simplify do anything here?
f_ctrs.init(args, ExprVector::new_col(Array<const ExprNode>(_f_ctr)).simplify(simpl_level));
assert(f_ctrs.expr().dim.size()==m);
}
}
Expand Down
2 changes: 1 addition & 1 deletion src/system/ibex_NormalizedSystem.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -40,7 +40,7 @@ class NormalizedSystem : public System {
* inequalities: f<=eps and -f<=eps. If eps==0
* equalities are duplicated.
*/
explicit NormalizedSystem(const System& sys, double eps=0, bool extended=false);
explicit NormalizedSystem(const System& sys, double eps=0, bool extended=false, int simpl_level=ExprNode::default_simpl_level);

/** Default epsilon applied to equations: 1e-8. */
static constexpr double default_eps_h = 1e-08;
Expand Down
2 changes: 2 additions & 0 deletions src/system/ibex_SystemMerge.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -25,6 +25,8 @@ class SystemMerge : public SystemFactory {

SystemMerge(const System& sys1, const System& sys2) {

set_simplification_level(0); // constraints do not need to be simplified again

SymbolMap<const ExprSymbol*> map;

/* the set of symbols of the resulting system,
Expand Down
2 changes: 1 addition & 1 deletion tests/Ponts30.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -252,7 +252,7 @@ void Ponts30::build_equ() {
equ.set_ref(i++,( A_y ));
equ.set_ref(i++,( A_x ));

f = new Function(symbols,ExprVector::new_col(equ).simplify(),"ponts30");
f = new Function(symbols,ExprVector::new_col(equ).simplify(ExprNode::default_simpl_level),"ponts30");
}

Ponts30::Ponts30() : init_box(30), hc4r_box(30,30), hc4_box(30) {
Expand Down
3 changes: 2 additions & 1 deletion tests/TestFunction.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -571,7 +571,8 @@ void TestFunction::def_domain01() {
void TestFunction::def_domain02() {
Function f("x","y","acos(x*sqrt(y))+y");
const System& sys=f.def_domain();
CPPUNIT_ASSERT(sameExpr(sys.f_ctrs.expr(),"(y;(1+(x*sqrt(y)));(-1+(x*sqrt(y))))"));
CPPUNIT_ASSERT(sameExpr(sys.f_ctrs.expr(),"(y;((x*sqrt(y))--1);((x*sqrt(y))-1))")); // simpl = 1
//CPPUNIT_ASSERT(sameExpr(sys.f_ctrs.expr(),"(y;(1+(x*sqrt(y)));(-1+(x*sqrt(y))))")); // simpl = 2
}

} // end namespace
2 changes: 1 addition & 1 deletion tests/TestNumConstraint.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,7 @@ void TestNumConstraint::build_from_string01() {
NumConstraint c("x","x+1<=2");

// CPPUNIT_ASSERT(sameExpr(c.f.expr(),"((x+1)-2)"));
CPPUNIT_ASSERT(sameExpr(c.f.expr(),"(-1+x)"));
CPPUNIT_ASSERT(sameExpr(c.f.expr(),"(x+-1)"));
CPPUNIT_ASSERT(c.op==LEQ);

} catch(SyntaxError&) {
Expand Down
20 changes: 11 additions & 9 deletions tests/TestParser.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -25,6 +25,8 @@ using namespace std;

namespace ibex {

static const int simpl = 2;

void TestParser::var01() {
System sys(SRCDIR_TESTS "/quimper/var01.qpr");
CPPUNIT_ASSERT(sys.args.size()==1);
Expand Down Expand Up @@ -235,7 +237,7 @@ void TestParser::ponts() {
}

void TestParser::choco01() {
System sys(2,"{1}+{0}=0");
System sys(2,"{1}+{0}=0", simpl);
CPPUNIT_ASSERT(sys.args.size()==2);
CPPUNIT_ASSERT(strcmp(sys.args[0].name,"{0}")==0);
CPPUNIT_ASSERT(strcmp(sys.args[1].name,"{1}")==0);
Expand All @@ -248,7 +250,7 @@ void TestParser::choco01() {

void TestParser::loop01() {
try {
System sys(SRCDIR_TESTS "/quimper/loop01.qpr");
System sys(SRCDIR_TESTS "/quimper/loop01.qpr", simpl);
cout << sys << endl;
double a = 1;
double b = 2;
Expand Down Expand Up @@ -287,7 +289,7 @@ void TestParser::loop01() {
}

void TestParser::error01() {
CPPUNIT_ASSERT_THROW(System(SRCDIR_TESTS "/quimper/error01.qpr"),SyntaxError);
CPPUNIT_ASSERT_THROW(System(SRCDIR_TESTS "/quimper/error01.qpr", simpl),SyntaxError);
}

void TestParser::issue245_1() {
Expand All @@ -296,11 +298,11 @@ void TestParser::issue245_1() {
}

void TestParser::issue245_2() {
CPPUNIT_ASSERT_THROW(System(SRCDIR_TESTS "/minibex/issue245_2.mbx"),SyntaxError);
CPPUNIT_ASSERT_THROW(System(SRCDIR_TESTS "/minibex/issue245_2.mbx", simpl),SyntaxError);
}

void TestParser::issue245_3() {
System sys(SRCDIR_TESTS "/minibex/issue245_3.mbx");
System sys(SRCDIR_TESTS "/minibex/issue245_3.mbx", simpl);
CPPUNIT_ASSERT(sameExpr(sys.ctrs[0].f.expr(),"((-3+(3*x^2))+y^2)"));
}

Expand Down Expand Up @@ -354,17 +356,17 @@ void TestParser::sum04() {
}

void TestParser::temp_in_loop() {
System sys(SRCDIR_TESTS "/minibex/issue380.mbx");
System sys(SRCDIR_TESTS "/minibex/issue380.mbx", simpl);
CPPUNIT_ASSERT(sameExpr(sys.f_ctrs.expr(),"((-1+x(1));(-2+x(2));(-3+x(3));(-4+x(4)))"));
}

void TestParser::diff_lock() {
System sys(SRCDIR_TESTS "/minibex/diff_lock.mbx");
CPPUNIT_ASSERT(sameExpr(sys.f_ctrs.expr(),"((2*x);((-3+y)+x^2))"));
System sys(SRCDIR_TESTS "/minibex/diff_lock.mbx", simpl);
CPPUNIT_ASSERT(sameExpr(sys.f_ctrs.expr(),"((2*x);((-3+x^2)+y))"));
}

void TestParser::issue365() {
System sys(SRCDIR_TESTS "/minibex/issue365.mbx");
System sys(SRCDIR_TESTS "/minibex/issue365.mbx", simpl);
CPPUNIT_ASSERT(sys.f_ctrs.expr().size==7);
}

Expand Down
2 changes: 1 addition & 1 deletion tests/TestSinc.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -58,7 +58,7 @@ void TestSinc::simplify() {
Interval cst(2,2);
const ExprConstant& x=ExprConstant::new_scalar(cst);
const ExprNode& y=ExprGenericUnaryOp::new_("sinc",x);
const ExprNode& z=y.simplify();
const ExprNode& z=y.simplify(ExprNode::default_simpl_level);
const ExprConstant* zz=dynamic_cast<const ExprConstant*>(&z);
CPPUNIT_ASSERT(zz!=NULL);
CPPUNIT_ASSERT(zz->get_value()==sinc(Interval(2,2)));
Expand Down
43 changes: 31 additions & 12 deletions tests/TestSystem.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -23,8 +23,12 @@ using namespace std;

namespace ibex {

static const int simpl = 2;

static System* sysex1() {
SystemFactory fac;
fac.set_simplification_level(simpl);

Variable x(3,"x");
Variable A(3,3,"A");
Variable y("y");
Expand All @@ -42,6 +46,8 @@ static System* sysex1() {

static System* sysex2() {
SystemFactory fac;
fac.set_simplification_level(simpl);

Variable x(3,"x");
Variable y("y");

Expand All @@ -58,6 +64,8 @@ static System* sysex2() {

static System* sysex3() {
SystemFactory fac;
fac.set_simplification_level(simpl);

Variable x("x");
Variable y("y");

Expand All @@ -72,7 +80,7 @@ static System* sysex3() {
}

void TestSystem::empty() {
System sys(SRCDIR_TESTS "/minibex/empty.mbx");
System sys(SRCDIR_TESTS "/minibex/empty.mbx", simpl);
CPPUNIT_ASSERT(sys.nb_ctr==0);
}

Expand Down Expand Up @@ -109,7 +117,7 @@ void TestSystem::factory01() {


void TestSystem::factory02() {
System sys(SRCDIR_TESTS "/quimper/unconstrained.qpr");
System sys(SRCDIR_TESTS "/quimper/unconstrained.qpr", simpl);

CPPUNIT_ASSERT(sys.nb_ctr==0);
CPPUNIT_ASSERT(sys.nb_var==2);
Expand Down Expand Up @@ -145,7 +153,7 @@ CPPUNIT_ASSERT(sys.ctrs[1].op==GEQ);
}

void TestSystem::copy02() {
System _sys(SRCDIR_TESTS "/quimper/unconstrained.qpr");
System _sys(SRCDIR_TESTS "/quimper/unconstrained.qpr", simpl);
System sys(_sys, System::COPY);

CPPUNIT_ASSERT(sys.nb_ctr==0);
Expand Down Expand Up @@ -193,7 +201,7 @@ CPPUNIT_ASSERT(sys.ctrs[1].op==EQ);

void TestSystem::extend01() {
System& _sys(*sysex2());
ExtendedSystem sys(_sys);
ExtendedSystem sys(_sys,0,simpl);
delete &_sys;

CPPUNIT_ASSERT(sys.nb_ctr==4);
Expand All @@ -206,7 +214,6 @@ CPPUNIT_ASSERT(sameExpr(sys.goal->expr(),"__goal__"));
//CPPUNIT_ASSERT(sys.goal==NULL);

CPPUNIT_ASSERT(sys.box.size()==5);

CPPUNIT_ASSERT(sys.ctrs.size()==4);
CPPUNIT_ASSERT(sys.f_ctrs.nb_arg()==3);
CPPUNIT_ASSERT(sys.f_ctrs.nb_var()==5);
Expand All @@ -222,8 +229,8 @@ CPPUNIT_ASSERT(sys.ctrs[3].op==LEQ);
}

void TestSystem::extend02() {
System _sys(SRCDIR_TESTS "/quimper/unconstrained.qpr");
ExtendedSystem sys(_sys);
System _sys(SRCDIR_TESTS "/quimper/unconstrained.qpr", simpl);
ExtendedSystem sys(_sys,0,simpl);

CPPUNIT_ASSERT(sys.nb_ctr==1);
CPPUNIT_ASSERT(sys.nb_var==3);
Expand All @@ -239,7 +246,7 @@ CPPUNIT_ASSERT(sys.ctrs[0].op==EQ);

void TestSystem::normalize01() {
System& _sys(*sysex3());
NormalizedSystem sys(_sys,0.5);
NormalizedSystem sys(_sys,0.5,false,simpl);
delete &_sys;

CPPUNIT_ASSERT(sys.nb_ctr==6);
Expand All @@ -252,10 +259,14 @@ void TestSystem::normalize01() {

// CPPUNIT_ASSERT(sameExpr(sys.ctrs[0].f.expr(),"((-1+x)+y)"));
// CPPUNIT_ASSERT(sameExpr(sys.ctrs[1].f.expr(),"((-1-x)-y)"));

// simpl=2

CPPUNIT_ASSERT(sameExpr(sys.ctrs[2].f.expr(),"((-1+x)-y)"));
CPPUNIT_ASSERT(sameExpr(sys.ctrs[3].f.expr(),"((-1-x)+y)"));
CPPUNIT_ASSERT(sameExpr(sys.ctrs[4].f.expr(),"((-0.5+x)-y)"));
CPPUNIT_ASSERT(sameExpr(sys.ctrs[5].f.expr(),"((-0.5-x)+y)"));

CPPUNIT_ASSERT(sys.ctrs[0].op==LEQ);
CPPUNIT_ASSERT(sys.ctrs[1].op==LEQ);
CPPUNIT_ASSERT(sys.ctrs[2].op==LEQ);
Expand All @@ -270,21 +281,23 @@ void TestSystem::normalize02() {
const ExprSymbol& y=ExprSymbol::new_("y");

SystemFactory fac;
fac.set_simplification_level(simpl);
fac.add_var(x);
fac.add_var(y);
const ExprNode& e=x+y;
Vector v(2);
v[0]=1; v[1]=2;
fac.add_ctr(((const ExprNode&) ExprVector::new_col(e,e))=ExprConstant::new_vector(v,false));
System sys(fac);
NormalizedSystem nsys(sys,1);
NormalizedSystem nsys(sys,1,false,simpl);
//CPPUNIT_ASSERT(sys.f_ctrs.expr().size==12); // the DAG structure not kept anymore with ExprSimplify2
CPPUNIT_ASSERT(sameExpr(nsys.ctrs[0].f.expr(),"(((-2+x)+y);((-3+x)+y))"));
CPPUNIT_ASSERT(sameExpr(nsys.ctrs[1].f.expr(),"(((-x)-y);((1-x)-y))"));
}

void TestSystem::merge01() {
SystemFactory fac1;
fac1.set_simplification_level(simpl);
{
Variable x("x");
Variable y(2,"y");
Expand All @@ -295,6 +308,7 @@ void TestSystem::merge01() {
System sys1(fac1);

SystemFactory fac2;
fac2.set_simplification_level(simpl);
{
Variable x("x");
Variable y(2,"y");
Expand All @@ -315,6 +329,7 @@ void TestSystem::merge01() {

void TestSystem::merge02() {
SystemFactory fac1;
fac1.set_simplification_level(simpl);
{
Variable x("x");
fac1.add_var(x);
Expand All @@ -323,6 +338,7 @@ void TestSystem::merge02() {
System sys1(fac1);

SystemFactory fac2;
fac2.set_simplification_level(simpl);
{
Variable x("x");
Variable y(2,"y");
Expand Down Expand Up @@ -353,6 +369,7 @@ void TestSystem::merge02() {

void TestSystem::merge03() {
SystemFactory fac1;
fac1.set_simplification_level(simpl);
{
Variable x("x");
fac1.add_var(x);
Expand All @@ -361,6 +378,7 @@ void TestSystem::merge03() {
System sys1(fac1);

SystemFactory fac2;
fac2.set_simplification_level(simpl);
{
Variable y(2,"y");
fac2.add_var(y);
Expand All @@ -378,9 +396,10 @@ void TestSystem::merge03() {


void TestSystem::merge04() {
System sys1(SRCDIR_TESTS "/minibex/I5.bch");
System sys2(SRCDIR_TESTS "/minibex/alkyl.bch");
System sys1(SRCDIR_TESTS "/minibex/I5.bch", simpl);
System sys2(SRCDIR_TESTS "/minibex/alkyl.bch", simpl);
System sys3(sys1,sys2);

CPPUNIT_ASSERT(strcmp(sys3.args[0].name,"x1")==0);
CPPUNIT_ASSERT(strcmp(sys3.args[9].name,"x10")==0);
CPPUNIT_ASSERT(strcmp(sys3.args[10].name,"x11")==0);
Expand All @@ -395,7 +414,7 @@ void TestSystem::merge04() {
}

void TestSystem::mutable_cst() {
System sys(SRCDIR_TESTS "/minibex/mutable_cst.mbx");
System sys(SRCDIR_TESTS "/minibex/mutable_cst.mbx", simpl);
sys.constant("a").i()=4;
sys.constant("b").v()[0]=5;
sys.constant("b").v()[1]=6;
Expand Down

0 comments on commit 4288495

Please sign in to comment.