Absolute value PL constraint (#228)

* initial abs cinstraint, three files - h, cpp and error

* variable name

* removing run3 files

* wip

* Sources.mk - add AbsConstraint.cpp; AbsConstraint.cpp - Add some signatures, fix satisfied(), implement getPossibleFixes()

* add constant ABS_CONSTRAINT_COMPARISON_TOLERANCE

* add ifndef to AbsConstraint.h

* add some signatures to AbsConstraint.h and fix some signatures at AbsConstraint.cpp

* fixing errors

* fix errors

* split and more

* add some signatures

* notify functions

* finsh write functions. next step - testing

* test file

* notifyLowerBound and notifyUpperBound

* test with sumathi

* add check at notify lower/upper bound if new bound is better then old bound. add some documentation

* getEntailedTightenings

* fix at notifyUpperBound

* Test to entailed_tighteningst

* duplicate and restore

* register_and_unregister

* test for notifyVariableValue, satisfied and updateVariableIndex

* more tests

* edit comments

* more tests

* some fixes

* some fixes

* fix

* add getter to _lowerBounds

* test_abs_entailed_tighteningst

* fix

* upper\lower bpound f <0 , get_upper_bound

* more testing and print func

* fix x_f<0

* fix x_f<0

* some changes

* some changes

* without test_abs_entailed_tighteningst2

* some changes if upper/ lower bound <0

* fix tighteningst2

* some fixes

* more tests for getEntailedTightenings

* add cases to getEntailedTightnings

* finish testing getEntailedTighteningsgit add Test_AbsConstraint.h!

* change non overlap at getEntailedTightenings

* change ovelap tests

* CMakeLists

* test fixes and case split

* fix

* finish tests

* abs_feasible_2 like relu_feasible_2

* add regress for abs constraint

* add some print at getEntailedTightening befor ASSERT

* notifynotifyLowerBound if var == _f && bound <0. i delete & bound ==0

* same as befor change not is posetive

* change the part when the bounds of _f need to be zero

* notifyLowerBound and upper, when update the prtner, if var is f, i add && bound>0

* test_abs_entailed_tighteningst0 if lower bound of f is <0

* check that _constraintBoundTightener exists before using it

* add test for _f bound<0

* more test lower bounf f<0

* 1 is UNSAT- not working, 2 is SAT

* getE fix overlap

* get lower bound, change to double

* more tests

* add feasible2

* non

* better printing of bounds

* without no overlap

* fix

* unsat

* more regress

* getEntailedTightenings without max positive

* fix a bug regarding bound extraction of fixed variables

* Entailed_Tightenings without max and min

* more regress

* match to tha changes at absconstraint

* without max/min at getEntailedTightenings

* match to changes at ans

* more regress

* add new files acas regress fixed input and with constraint. inputQuery fix typo

* check correctness

* fix the new network, but there is steal problem

* fix the new network, but there is yet problem

* change fix point

* configuration

* fix acas abs constraint

* add for at the main, add documentaion

* coding style

* changes

* minor

* the old regression test moved to be a system test

* moving some files around

* typo

* compilation issues

* cleanup

* cleanup

* refactoring

* finished pass on main class

* remove AbsError class

* compilation

* thorough phass over the unit tests

* more polishing of bound tighting and phase-fixing-detection

* system test cleanup

* dont override variable elimination

* additional tests

* some more cleanup

* remove a few comments

* Merge from master (#231)

* Use ndebug (#229)

Used NDEBUG flag to indicate of not debug mode (CMake adds this flag be default in release mode)
Default compilation is release mode

* Cmake: Minor (#230)

* fix a couple of warnings

* minor

Co-authored-by: yuvaljacoby <yuvaljacoby@users.noreply.github.com>
Co-authored-by: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com>

* bug fix

* remove "unused"s

* minor

* Aleks' comments

* space

* test no longer needed

Co-authored-by: shirana <shiran.aziz@gmail.com>
Co-authored-by: Christopher Lazarus <clazarusg@gmail.com>
Co-authored-by: Guy Katz <guykatz@cs.huji.ac.il>
Co-authored-by: yuvaljacoby <yuvaljacoby@users.noreply.github.com>
Co-authored-by: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com>

src/configuration/GlobalConfiguration.cpp

@@ -69,6 +69,7 @@ const double GlobalConfiguration::PSE_GAMMA_ERROR_THRESHOLD = 0.001;
 const double GlobalConfiguration::PSE_GAMMA_UPDATE_TOLERANCE = 0.000000001;
 
 const double GlobalConfiguration::RELU_CONSTRAINT_COMPARISON_TOLERANCE = 0.001;
+const double GlobalConfiguration::ABS_CONSTRAINT_COMPARISON_TOLERANCE = 0.001;
 
 const bool GlobalConfiguration::ONLY_AUX_INITIAL_BASIS = false;
 

src/configuration/GlobalConfiguration.h

@@ -131,9 +131,12 @@ class GlobalConfiguration
     // PSE's Gamma function's update tolerance
     static const double PSE_GAMMA_UPDATE_TOLERANCE;
 
-    // The tolerance for checking whether f = Relu( b ), to determine a ReLU's statisfaction
+    // The tolerance for checking whether f = Relu( b )
     static const double RELU_CONSTRAINT_COMPARISON_TOLERANCE;
 
+    // The tolerance for checking whether f = Abs( b )
+    static const double ABS_CONSTRAINT_COMPARISON_TOLERANCE;
+
     // Should the initial basis be comprised only of auxiliary (row) variables?
     static const bool ONLY_AUX_INITIAL_BASIS;