3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-19 12:23:38 +00:00

SLS refactoring

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2014-03-19 17:26:05 +00:00
parent 7451e5cae0
commit 13307a1d51

View file

@ -18,6 +18,10 @@ Notes:
This file should go away completely once we have evaluated all options. This file should go away completely once we have evaluated all options.
--*/ --*/
#ifndef _SLS_COMPILATION_SETTINGS_H_
#define _SLS_COMPILATION_SETTINGS_H_
// which unsatisfied assertion is selected? only works with _FOCUS_ > 0 // which unsatisfied assertion is selected? only works with _FOCUS_ > 0
// 0 = random, 1 = #moves, 2 = assertion with min score, 3 = assertion with max score // 0 = random, 1 = #moves, 2 = assertion with min score, 3 = assertion with max score
#define _BFS_ 0 #define _BFS_ 0
@ -155,4 +159,6 @@ InvalidConfiguration;
#endif #endif
#if (_PERC_STICKY_ && !_FOCUS_) #if (_PERC_STICKY_ && !_FOCUS_)
InvalidConfiguration; InvalidConfiguration;
#endif
#endif #endif