[TG-925] Add command line options for setting up satcheck randomizer #1501

LAJW · 2017-10-19T15:22:51Z

New options:

--random-seed 13121110 # seed for randomizer - floating point number
--random-var-freq 0...1 # random generator frequency - floating point number

If unset defaults those values as defined in sat checker (works as before).

Also simplifies the satcheck wrapper implementation.

Review tips: Each commit contains changes as described in the title. There's one massive commit, which forces parametrization of satcheck. I tried to make it as small as possible, given in how many places satcheck is used.

TODO: Prettier messages if arguments are not valid, ~~floating point numbers, restrict random-var-freq to 0...1 in command line parser, lintage.~~

Implements this ticket: https://diffblue.atlassian.net/browse/TG-925

LAJW · 2017-10-19T15:24:25Z

@antlechner Checkout the branch, see if it does what you think it should.
@allredj Take a look.

tautschnig

I have serious concerns about the design used here as detailed, and I have several "Why?" questions. The true blocker, however, is making it impossible to use any other solver than MiniSat2.

tautschnig · 2017-10-19T17:06:32Z

src/solvers/sat/satcheck_minisat2.cpp

-  add_variables();
-  solver->setPolarity(a.var_no(), value);
-}
-


Mind explaining what is broken about this?

tautschnig · 2017-10-19T17:08:46Z

src/solvers/sat/satcheck_minisat2.cpp

@@ -310,13 +287,13 @@ void satcheck_minisat_simplifiert::set_frozen(literalt a)
  if(!a.is_constant())
  {
    add_variables();
-    solver->setFrozen(a.var_no(), true);
+    static_cast<Minisat::SimpSolver*>(solver)->setFrozen(a.var_no(), true);


Why is this better than the previous code?

The only point of CRTP and declaring every single member as a template was to avoid a single cast. With virtual functions on top it is rather difficult to read. If you still don't like this raw cast could be wrapper in a method.

The intended use of CRTP is to avoid code duplication between unrelated classes while avoiding virtual functions in performance critical code. Since class was already virtual, there was no point in using CRTP here.

FWIW I don't see how class satcheck_minisat_no_simplifiert: public satcheck_minisat2_baset<Minisat::Solver> ever was an instance of CRTP. There was a templated base class that could be instantiated in a number of ways. What happened was that not all instantiations would support the full interface. That seemed like a perfectly legitimate use of templates and template instantiation to me?

tautschnig · 2017-10-19T17:14:47Z

src/goto-instrument/accelerate/accelerate.cpp

+int acceleratet::accelerate_loop(
+  goto_programt::targett &loop_header,
+  const double random_seed,
+  const double random_var_freq)


There is some design problem here: passing in completely unrelated options to some function. At bare minimum pass along optionst so that it isn't necessary to add one parameter for each future option.

The design problem is that the number of arguments might grow in the future. I agree.

But I think that concerns should remain separated. Minisat should not parse command line arguments. I'd humbly suggest passing a reference to typed "config" struct. Which in this case would take only 2 arguments.

I largely don't mind whether it's an optionst passed around (optionst being the result of parsed cmdlinet arguments) or actually going for config, which is global anyway and would drastically reduce the size of this PR.

Globals are not a solution. Since every object (and many functions) requires its own, often large configuration, storing all arguments in a global uncategorized, untyped hashmap would be an architectural disaster.

Globals are not an answer. Better parsing and grouping is.

Globals are what we have at the moment. Whether we should have them or not is a different question to implementing this feature.

FWIW: "storing all arguments in a global uncategorized, untyped hashmap would be an architectural disaster." is not what configt is/does.

tautschnig · 2017-10-19T17:16:05Z

src/solvers/sat/satcheck_minisat2.cpp

@@ -29,6 +29,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #error "Expected HAVE_MINISAT2"
 #endif

+const double satcheck_minisat2_baset::default_random_seed=91648253.;


Where does this magic number come from? Explain and move it to util/magic.h.

It was copied from minisat2 internals.

tautschnig · 2017-10-19T17:18:25Z

src/solvers/sat/satcheck_minisat2.cpp

@@ -47,14 +47,14 @@ tvt satcheck_minisat2_baset::l_get(literalt a) const

  tvt result;

-  if(a.var_no()>=(unsigned)solver->model.size())
+  if(a.var_no()>=(unsigned)solver_->model.size())


GitHub, Vim, Emacs, Visual Studio, QT, VS Code and AFAIK Clion do not highlight member variables or member functions. C++ does not enforce this->. Therefore it's often difficult to discern whether a variable is a member or local. Every time such variable is encountered, the reader has to spend considerable amount of time going through the entire file looking for globals, statics, members and/or child classes.

We've spent months arguing about this and finally postfix underscore was agreed upon to signify a member variable. On top of that solver_ was already used as an argument name.

Where is this documented in the coding standard?

At the same time: this PR is already way too large, why include such style changes in there?

tautschnig · 2017-10-19T17:20:02Z

src/solvers/sat/satcheck_minisat2.cpp

-}
-
-#endif
-


This has only been added as recently as 0ee4933 - maybe just revert the entire commit (assuming @smowton approves)?

It might be a part of an experiment to stop perl script with CTRL+C (which only had to be implemented in the perl script).

No, it was intended to facilitate input synthesis, the idea being if you're using a sub-solver to synthesise inputs then you should only give it a little time, since it's not worth losing your solution because of an input synthesis timeout. However there turned out to be too many sources of possible timeouts in CBMC to be practical, so I concluded we should do this by splitting the test-generation process into multiple processes and use process granularity crash/timeout isolation instead.

Long story short, revert that commit at your leisure.

tautschnig · 2017-10-19T17:21:09Z

src/solvers/sat/satcheck_minisat2.cpp

@@ -32,7 +32,7 @@ Author: Daniel Kroening, kroening@kroening.com
 const double satcheck_minisat2_baset::default_random_seed=91648253.;
 const double satcheck_minisat2_baset::default_random_var_freq=0.;

-void convert(const bvt &bv, Minisat::vec<Minisat::Lit> &dest)
+static void convert(const bvt &bv, Minisat::vec<Minisat::Lit> &dest)


What is the rationale for "stacheck_minisat2_baset - refactor prop_solve " ?

tautschnig · 2017-10-19T17:24:39Z

src/solvers/refinement/bv_refinement.h

@@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/ui_message.h>

 #include <solvers/flattening/bv_pointers.h>
+#include <solvers/sat/satcheck_minisat2.h>


This implies that no solver other than Minisat2 could be used. This is certainly a blocker.

Suggested move of constant definitions to the constant file should alleviate that.

Yep; that's a blocker for several other industrial users.

martin-cs · 2017-10-19T19:30:22Z

@tautschnig : The why, @antlechner can best explain, but they were after a low cost way of getting a variety of models. We had a long discussion including my reservations about the amount of variation vs. performance trade-off and that universal hashing is actually the best way of get model variety. However we felt that as a hidden option, it was relatively low harm.

The PR does not look anything like the minimum code required to implement this feature. It seems to mix up refactorings, code removal, new features and so on, while breaking various interfaces and supporting code. As such I would oppose it's merge in the current form.

martin-cs

Start from a blank sheet and see how small (in lines of code) you can make the diff.

martin-cs · 2017-10-19T19:34:30Z

src/cbmc/cbmc_parse_options.cpp

@@ -994,6 +1001,8 @@ void cbmc_parse_optionst::help()
    " --object-bits n              number of bits used for object addresses\n"
    " --dimacs                     generate CNF in DIMACS format\n"
    " --beautify                   beautify the counterexample (greedy heuristic)\n" // NOLINT(*)
+    " --random-seed %f             SAT checker randomizer seed\n" // NOLINT(*)


Seed should probably be treated as an opaque 64 bit bit-vector. Minisat's use of it as a double is just implementational convenience. If we use it to seed other random number generators such as srand() (which is probably a good idea) they will want it as an integer.

martin-cs · 2017-10-19T19:35:26Z

src/cbmc/cbmc_parse_options.cpp

+  if (cmdline.isset("random-var-freq"))
+    options.set_option(
+      "random-var-freq", cmdline.get_values("random-var-freq"));
+


These could have default values set here. This is especially useful for random-seeds.

martin-cs · 2017-10-19T19:37:01Z

src/cbmc/cbmc_parse_options.cpp

@@ -994,6 +1001,8 @@ void cbmc_parse_optionst::help()
    " --object-bits n              number of bits used for object addresses\n"
    " --dimacs                     generate CNF in DIMACS format\n"
    " --beautify                   beautify the counterexample (greedy heuristic)\n" // NOLINT(*)
+    " --random-seed %f             SAT checker randomizer seed\n" // NOLINT(*)
+    " --random-var-freq %f         SAT checker randomization frequency\n" // NOLINT(*)
    " --localize-faults            localize faults (experimental)\n"


I'm not sure we use "%" in other options.

martin-cs · 2017-10-19T19:37:48Z

src/cbmc/cbmc_solvers.cpp

+  if(options.get_bool_option("random-var-freq"))
+    random_var_freq=std::stod(options.get_option("random-var-freq"));
+  return { random_seed, random_var_freq };
+}


Option parsing shouldn't be done here.

martin-cs · 2017-10-19T19:38:43Z

src/cbmc/cbmc_solvers.cpp


-  solver->prop().set_message_handler(get_message_handler());
+  solver->set_prop(make_satcheck(options, use_simplifier, get_message_handler()));


Frankly this all seems a bit unnecessary.

martin-cs · 2017-10-19T19:49:02Z

src/solvers/refinement/string_refinement.cpp

@@ -1935,7 +1935,7 @@ static optionalt<exprt> find_counter_example(
  const exprt &axiom,
  const symbol_exprt &var)
 {
-  satcheck_no_simplifiert sat_check;
+  satcheck_no_simplifiert sat_check(0., 0.);
  bv_refinementt::infot info;


How are these values related to the satcheck_minisat2_baset::default_random_seed. Also, this is probably the one place this patch is actually needed.

martin-cs · 2017-10-19T19:49:21Z

src/solvers/sat/satcheck_minisat2.cpp

@@ -28,7 +29,10 @@ Author: Daniel Kroening, kroening@kroening.com
 #error "Expected HAVE_MINISAT2"
 #endif

-void convert(const bvt &bv, Minisat::vec<Minisat::Lit> &dest)
+const double satcheck_minisat2_baset::default_random_seed=91648253.;


Why this number?

martin-cs · 2017-10-19T19:51:54Z

src/solvers/sat/satcheck_minisat2.cpp


 void satcheck_minisat_simplifiert::set_frozen(literalt a)
 {
  if(!a.is_constant())
  {
    add_variables();
-    solver->setFrozen(a.var_no(), true);
+    static_cast<Minisat::SimpSolver*>(solver_.get())->setFrozen(a.var_no(), true);
  }


How is this an improvement?

martin-cs · 2017-10-19T19:53:32Z

src/solvers/sat/satcheck_minisat2.cpp

  }
 }

 bool satcheck_minisat_simplifiert::is_eliminated(literalt a) const
 {
  assert(!a.is_constant());

-  return solver->isEliminated(a.var_no());
+  return static_cast<const Minisat::SimpSolver*>(solver_.get())->
+    isEliminated(a.var_no());
 }


There seem to be an awful lot of "refactorings" here which are not related to the actual PR. Please do not do this. Refactorings should be a separate commit.

It should be said that @LAJW has done this in a pretty clean series of commits. I do not know what the exact request in TG-925 is; if it is what the PR subject says, then surely refactorings have no place in here. If TG-925 requested refactoring, then these should be better be considered for other solvers as well.

martin-cs · 2017-10-19T19:58:31Z

src/solvers/sat/satcheck_minisat2.h

+private:
+  resultt prop_solve_impl();
+
+  bvt assumptions_;


Why rename variables? Our coding standard doesn't require private variables to be named with underscores.

smowton · 2017-10-20T09:13:07Z

@tautschnig @martin-cs in defence of parameterising from above (threading an option through from driver to user class) as opposed to global parameters, there have already been several cases in the unit tests where changes to config accidentally spilled into neighbouring tests, leading to surprising breakages depending on the order the tests happened to run; similarly when designing the input synthesis solver (which admittedly I now advocate pushing into a separate process for performance reasons) I was repeatedly tripped by an apparently-clean solvert instance inheriting a previous session's configuration via config. There are surely similar tripwires lurking for future developers when information flow is hidden. Whether or not we want to port the existing config settings, I advocate adding new ones to some solver_configt and passing that into classes that need a solver such that the scope of their effect is clear.

tautschnig · 2017-10-20T10:35:36Z

On the global-config-object story: I very much agree that global objects are bad, and removing config from solvers has already been happening as far as possible. I fully support any attempt towards "solver options" or the likes. What I cannot agree to is explicitly listing all options that may pop up, and may in fact only be useful for selected solvers, as parameters to all bits of code that eventually create a solver object. This would yield an endless stream of changes of the same size as this PR, and that is clearly unhealthy.

martin-cs · 2017-10-20T10:44:25Z

On Fri, 2017-10-20 at 02:13 -0700, Chris Smowton wrote: @tautschnig @martin-cs in defence of parameterising from above (threading an option through from driver to user class)

( This wasn't quite what I meant when I was talking about above or below. That's not an issue, this is worth talking about independently but I thought I should clarrify / separate the two. I was simply talking about whether the default values were set. )

as opposed to global parameters, there have already been several cases in the unit tests where changes to `config` accidentally spilled into neighbouring tests;

Interesting; I haven't looked at this code much.

similarly when designing the input synthesis solver (which admittedly I now advocate pushing into a separate process for performance reasons) I was repeatedly tripped by an apparently-clean `solvert` instance inheriting a previous session's configuration via `config`. There are surely similar tripwires lurking for future developers when information flow is hidden. Whether or not we want to port the existing `config` settings, I advocate adding new ones to some `solver_configt` and passing that into classes that need a solver.

I think we need a separate issue to discuss how config management should be done. This is a discussion worth having but it is massively off-topic here. It should not be part of this PR. Cheers, - Martin

LAJW · 2017-10-20T18:15:55Z

Removed all refactors.

@martin-cs @tautschnig @smowton @thk123 Review please.

tautschnig

I do like this version much better, but a final fix to avoid linking failures if a SAT solver other than MiniSat2 is being used will be required.

FWIW, the huge amount of changes to loop acceleration highlight a design problem in that code, which the changes proposed now are just a symptom of.

tautschnig · 2017-10-20T18:23:26Z

src/solvers/sat/satcheck_minisat2.h

+  /// Parse satcheck options
+  /// \param options Options object
+  /// \return An instance of satcheck_minisat_info object
+  static satcheck_minisat_infot parse(const optionst &options);


How about making this a constructor (in addition to a default constructor)?

I wanted to use a function, but assigning a function pointer behind an ifdef proved to be a little too cumbersome.

I'm sure you've got good reasons for not doing it, but I don't really understand your explanation as I don't know which function pointer or ifdef that would be?

The one in satcheck.h which switches between solvers. I'd have to create another one in .cpp file I think.

How about declaring the interface in satcheck.h and then provide an implementation in each solver? Thus different solvers could happily parse/ignore different options? Maybe that's a bad idea for other reasons?

I think it's "beyond the scope of this PR". The common interface isn't specified anywhere, macros just switch between different typedefs.

tautschnig · 2017-10-20T18:29:43Z

src/goto-instrument/goto_instrument_parse_options.cpp

+        satcheck_info.random_var_freq
+          =std::stod(cmdline.get_value("random-var-freq"));
+      accelerate_functions(
+        goto_model, cmdline.isset("z3"), satcheck_info);


The command-line options are never added to goto-instrument, are they? It seems they just exist in cbmc.

tautschnig · 2017-10-20T18:31:17Z

src/solvers/sat/satcheck_minisat2.h

@@ -23,6 +23,12 @@ class Solver; // NOLINT(readability/identifiers)
 class SimpSolver; // NOLINT(readability/identifiers)
 }

+struct satcheck_minisat_infot final


This file will only be included when SATCHECK_MINISAT2 is defined, hence all other cases will cause linking failures under the subsequent commits.

smowton

LGTM, one documentation suggestion

smowton · 2017-10-21T10:36:20Z

src/cbmc/cbmc_solvers.cpp

-  }();
-
-  prop->set_message_handler(get_message_handler());
+  const bool use_simplifier=options.get_bool_option("sat-preprocessor");


Suggest commenting that this definition intentionally differs from the one on line 115

kroening · 2017-10-21T11:01:44Z

Why is it desirable to randomise SAT?

smowton · 2017-10-21T11:04:13Z

@kroening AFAIK the goal is to encourage alternate test-cases and thus fuzz the validity of the Java models

kroening · 2017-10-21T11:09:17Z

Randomizing the solver is really not how this should be attempted to be achieved.

smowton · 2017-10-21T11:14:38Z

@kroening that discussion has already been around a few times -- see Martin's comment here #1501 (comment) for example

thk123 · 2017-10-23T10:41:09Z

I don't think I have the knowledge of the relevant files in this PR for which I am a code owner. Happy to review if needed, but looks like plenty of eyes are already going through this.

romainbrenguier

I reviewed only the changes in src/solvers and they make sense for me.

romainbrenguier · 2017-10-23T13:32:40Z

src/solvers/sat/satcheck_minisat2.cpp

 {
+  if(info.random_var_freq<0. || 1.<info.random_var_freq)
+    throw std::invalid_argument(
+      "random_var_freq should be a floating point number between 0 and 1");


Could this check be done in parse instead?

kroening · 2017-10-23T15:08:12Z

Does that need to be in CBMC? Not just testgen?

kroening · 2017-10-23T15:10:21Z

Also, the use-case does not justify changing the API.
There must be constructors that produce the current behaviour without the satcheck_info.

LAJW · 2017-10-23T15:23:05Z

@kroening The satcheckers themselves are hidden behind those wrappers. The only way to add extra options is to modify wrappers. But each wrapper has to have its own set of arguments, as each solver is different.

satcheck_infot - @tautschnig pointed out that it's a bad idea to pull those arguments explicitly, and they should be grouped and passed together to the solver.

In general I like to create _info struct for functions exceeding 3 arguments. With C++11 in-header initialisers it's possible to assign sensible defaults to unassigned fields. structs can also be composed, so often constructors can accept less arguments. Also new arguments can be easily added, and looking for function documentation is no longer necessary to figure out which value is set to which argument. Better solution is coming to C++20, but for now this is the best tool available.

LAJW · 2017-10-23T16:08:39Z

@tautschnig The remaining satcheckers' interfaces have been updated to work with the _infot struct.

LAJW · 2017-10-24T12:39:31Z

@tautschnig @martin-cs @thk123 Please, re-review.

tautschnig · 2017-10-27T14:54:37Z

src/solvers/sat/satcheck_minisat2.h

+  /// \return An instance of satcheck_minisat_info object
+  static satcheck_minisat_infot parse(const optionst &options);
+  size_t random_seed=91648253; // Default copied from minisat2
+  double random_var_freq=0.;


As these have default values, wouldn't it be possible to follow @kroening consideration to maintain the existing interface of solvers that can be default-constructed without such options?

tautschnig · 2017-10-27T14:58:02Z

Does that need to be in CBMC? Not just testgen?

Does testgen invoke CBMC, or is it a new command-line front end? If the latter is the case, then indeed I don't understand why the changes have been implemented as is done here. Back in my work on FShell I never made any modifications to CBMC, but just derived my own implementations of classes as needed (for example for computing multiple test inputs covering the same test goals).

peterschrammel · 2017-10-27T15:37:19Z

I think this PR mixes up two issues that should be done independently:

Providing a seed (and other randomisation) options to the sat solver
Refactoring the way how we create and configure solver instances

I'd suggest to do only 1. here, which should probably be done by using similar mechanisms as already available in propt for setting assumptions, e.g. add a function set_seed and a function has_set_seed. The only other changes besides adding the command line options are then overriding these functions in the minisat wrapper and calling them from cbmc_solvers. I think that this is the least invasive solution.

Improving 2. is a different story that should be discussed elsewhere. I'm very much in favour of having a generic configuration data structure that replaces optionst (and configt and other integers and flags passed around) that is built in *_parse_optionst and passed down to the various components of the system (#1319 could be a candidate for doing that). cbmc_solvers should be moved to solvers/ so that it can be used by all tools and should be the only interface for constructing a solver instance.

peterschrammel · 2017-11-10T22:36:01Z

src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.h

    symbol_table(_symbol_table),
    ns(symbol_table),
    goto_functions(_goto_functions),
    goto_program(_goto_program),
    loop(_loop),
    loop_header(_loop_header),
-    utils(symbol_table, goto_functions, loop_counter)
+    utils(symbol_table, goto_functions, loop_counter),
+    satcheck_info_(satcheck_info)


Underscores at the beginning, underscores at the end... -- this is super-inconsistent. Please follow the style of the code that you are editing instead of making it incoherent on purpose!

peterschrammel · 2017-11-10T22:42:06Z

src/solvers/prop/prop.h

@@ -116,6 +116,11 @@ class propt:public messaget, public prop_assignmentt
    warning() << "CPU limit ignored (not implemented)" << eom;
  }

+  /// Set Random variable frequency (Exclusive to minisat2)
+  virtual void random_var_freq(std::size_t i) { }
+  /// Set Random variable seed (Exclusive to minisat2)


Also glucose supports both settings. I suggest to add a has_random_seed() etc so that cbmc_solvers can check whether the selected solver supports the feature and can output an appropriate error message.

peterschrammel · 2017-11-10T22:45:34Z

src/goto-instrument/goto_instrument_parse_options.cpp

+        options.set_option(
+          "random-var-freq", cmdline.get_value("random-var-freq"));
+      accelerate_functions(
+        goto_model, cmdline.isset("z3"), parse_satcheck_info(options));


This is a weird way of doing that. I suggest to pass optionst only and sort out the mess inside accelerate_functions.

peterschrammel · 2017-11-10T22:54:44Z

src/solvers/sat/satcheck_minisat2.cpp

@@ -253,8 +254,8 @@ void satcheck_minisat2_baset<T>::set_assignment(literalt a, bool value)
 }

 template<typename T>
-satcheck_minisat2_baset<T>::satcheck_minisat2_baset(T *_solver):
-  solver(_solver), time_limit_seconds(0)
+satcheck_minisat2_baset<T>::satcheck_minisat2_baset(T* solver_):


This is unnecessary and violates coding style. Please undo.

peterschrammel · 2017-11-10T22:56:32Z

src/util/options.cpp

@@ -81,3 +82,14 @@ const optionst::value_listt &optionst::get_list_option(
  else
    return it->second;
 }
+
+satcheck_infot parse_satcheck_info(const optionst &options)


This cannot live here. Move to solvers/sat

peterschrammel · 2017-11-10T22:58:08Z

src/solvers/prop/prop.h

@@ -116,6 +116,11 @@ class propt:public messaget, public prop_assignmentt
    warning() << "CPU limit ignored (not implemented)" << eom;
  }

+  /// Set Random variable frequency (Exclusive to minisat2)
+  virtual void random_var_freq(std::size_t i) { }


Rename to set_random_var_freq for consistency.

peterschrammel · 2017-11-10T22:58:16Z

src/solvers/prop/prop.h

+  /// Set Random variable frequency (Exclusive to minisat2)
+  virtual void random_var_freq(std::size_t i) { }
+  /// Set Random variable seed (Exclusive to minisat2)
+  virtual void random_seed(std::size_t i) { }


Rename to set_random_seed for consistency.

peterschrammel · 2017-12-02T10:52:20Z

@LAJW, please rebase and fix the linting issues.

peterschrammel · 2017-12-02T11:10:04Z

src/cbmc/cbmc_parse_options.cpp

@@ -906,123 +913,178 @@ void cbmc_parse_optionst::help()

  std::cout << "   * *\n";

-  std::cout <<


Please exclude the help text from clang-formatting (// clang-format off/on)

peterschrammel · 2017-12-02T11:10:50Z

src/cbmc/cbmc_parse_options.h

@@ -24,47 +24,48 @@ class bmct;
 class goto_functionst;
 class optionst;

-#define CBMC_OPTIONS \


Please exclude this from clang-formatting

peterschrammel · 2017-12-02T11:12:47Z

src/cbmc/cbmc_solvers.cpp

+  else
+    satcheck = util_make_unique<satcheck_no_simplifiert>();
+  satcheck->set_message_handler(message_handler);
+  satcheck->set_random_seed(satcheck_info.random_seed);


I suggest to check here whether the solver has the feature (satcheck->has_random_seed() and output an error message otherwise. Alternatively, at least output a warning in the base class (see below).

Warning added.

peterschrammel · 2017-12-02T11:16:48Z

src/solvers/prop/prop.h

@@ -116,6 +116,15 @@ class propt:public messaget, public prop_assignmentt
    warning() << "CPU limit ignored (not implemented)" << eom;
  }

+  /// Set random variable frequency (Exclusive to minisat2)


Also glucose has this feature. Output at least a warning if the solver does not implement this feature.

Glucose build doesn't seem to want to work, I'm not sure which parameters to add. I'm skipping it. Maybe we can add this later.

Not sure which problem you've run into, but marek-trtik@2548e7f might be helpful.

peterschrammel · 2017-12-02T11:22:18Z

src/solvers/sat/satcheck_minisat2.h

@@ -51,6 +53,9 @@ class satcheck_minisat2_baset:public cnf_solvert
    time_limit_seconds=lim;
  }

+  void set_random_var_freq(std::size_t) override;


Do the same for glucose to see whether this can be used with at least two solvers without hiccup.

LAJW · 2017-12-11T13:18:59Z

@peterschrammel Rebased, fixed lintage, added warning. I don't know how to test the glucose changes, so not adding them.

peterschrammel · 2018-01-04T20:51:07Z

@martin-cs, @tautschnig, I cleaned this up a bit and pulled apart the two purposes of this PR (1. randomisation, 2. unify solver instantation). I recommend reviewing the commits related to these two purposes separately. I think it's a bit clearer now, but mixing up 1. and 2. is still quite distracting - let me know if I should create two PRs instead.
To further improve 2. I propose a refactoring #1700 (to come in a follow-up PR).

tautschnig · 2018-01-04T22:15:10Z

src/cbmc/cbmc_solvers.cpp

+    satcheck = util_make_unique<satcheck_no_simplifiert>();
+  satcheck->set_message_handler(message_handler);
+  satcheck->set_random_seed(satcheck_info.random_seed);
+  satcheck->set_random_var_freq(satcheck_info.random_var_freq);


So this will always attempt to set the random_var_freq even if neither the solver supports it nor the user ever requested it? The resulting warning will be rather confusing to the user, isn't it?

With all the updates by @LAJW and discussion (thanks!) this is the only remaining blocker for me.

tautschnig · 2018-01-04T22:18:14Z

src/solvers/sat/satcheck.cpp

+{
+  satcheck_infot satcheck_info;
+  if(!options.get_option("random-seed").empty())
+    satcheck_info.random_seed = std::stoul(options.get_option("random-seed"));


Use safe_string2size_t as sizeof(unsigned long)!=sizeof(std::size_t) on Windows.

Good catch. But why not stoull (unsigned long long)?

Because that wouldn't be correct on 32-bit architectures as sizeof(unsigned long long)!=sizeof(std::size_t) on those?

tautschnig · 2018-01-04T22:19:46Z

src/solvers/sat/satcheck_minisat2.cpp

-  solver(_solver), time_limit_seconds(0)
+template <typename T>
+satcheck_minisat2_baset<T>::satcheck_minisat2_baset(T *_solver)
+  : solver(_solver), time_limit_seconds(0)


Whitespace changes?

tautschnig · 2018-01-04T22:20:07Z

src/solvers/sat/satcheck_minisat2.cpp

-satcheck_minisat_simplifiert::satcheck_minisat_simplifiert():
-  satcheck_minisat2_baset<Minisat::SimpSolver>(new Minisat::SimpSolver)
+satcheck_minisat_simplifiert::satcheck_minisat_simplifiert()
+  : satcheck_minisat2_baset<Minisat::SimpSolver>(new Minisat::SimpSolver())


Whitespace changes?

tautschnig · 2018-01-04T22:29:52Z

src/solvers/prop/prop.h

+  virtual void set_random_var_freq(double value)
+  {
+    warning() << "random-var-freq not supported" << eom;
+  }


Design idea/question: instead of introducing a new set_... function for each future option, can't we have a prop_configt made up of optionalt<T> fields (presently an optionalt<std::size_t> and an optionalt<double>) and one set_config(prop_configt)? The default implementation here would then check each field for being none, and else yield a warning. That would also address one of my comments made elsewhere.

I think @peterschrammel might want to answer this question.

I am against introducing more and more custom configuration classes: They are likely to become incompatible with each other, requiring to copy/adapt configuration data at interfaces.
I'm in favour of having a single dictionary-like data structure such as optionst, which is passed along throughout the codebase and carries all the configuration data. Optionst should be enhanced with proper 'optional' behaviour and a way to override individual items without requiring a full copy. @LAJW had a go at such an optionst replacement some time ago (#1319).

For this PR, I could propose to get rid of set_* functions and replace them by an optionst-based solution.

Isn't satcheck_infot such a custom configuration class? I was just thinking to move this to propt. My rationale being the present need to add additional set_... calls at each site whenever new ones are added, plus the problem that there may be spurious warnings as said in my other comment: #1501 (comment)

@peterschrammel Map from #1319 is an overkill. If you want dictionaries, just use std::unordered_map. I'm in favour of structs, as they lean towards parsing done in one spot, rather than spreading throughout the entire application (they separate UI from business logic). It's bad enough that we print to standard output all over the place, I didn't want to contribute to the problem.

satcheck_infot was a common satcheck constructor argument in one of the earlier revisions of this PR. If we truly cannot change satcheck constructor signature, then putting that as a set_config method (which would serve the role of a constructor) might be the next best thing.

It doesn't matter what is the name of the class to which we're printing. The fact that we're printing raw strings right next to the business logic is the problem.

So what would you be doing instead?

If it were up to me, I'd build a view instead and delegate formatting to that. View would be passed as argument or functions could return what to print to view as their result. Views could easily be swapped (CLI/JSON/Dummy, etc.). But it's not up to me.

Constructive ideas will always be appreciated, rambling less so. Everyone should feel empowered to create an issue to trigger discussion, or directly start with a pull request (at the risk of it being handed back for major rework).

Supposedly it is up to a message handler to take care of formatting. Surely that isn't fully done this way and needs fixing (hence, e.g., #1359). Yet your comments sound like you see a need for much bigger changes?

So what would you be doing instead?

You've requested my opinion, I gave it to you. Yes, slightly bigger changes than just hotfixes.

But I think we've strayed much too far away from the original point, and it's up to @peterschrammel to decide how he would like argument passing to look like. Current state is what he specifically requested, so I'm not going to go against his design.

tautschnig · 2018-01-04T22:33:52Z

src/goto-instrument/accelerate/acceleration_utils.h

+  bool do_assumptions(
+    std::map<exprt, polynomialt> polynomials,
+    patht &body,
+    exprt &guard);


Whitespace change

tautschnig · 2018-01-04T22:34:09Z

src/goto-instrument/accelerate/acceleration_utils.h

@@ -66,8 +71,7 @@ class acceleration_utilst
                          std::set<std::pair<expr_listt, exprt> > &coefficients,
                          polynomialt &polynomial);

-  bool check_inductive(std::map<exprt, polynomialt> polynomials,
-                       patht &path);
+  bool check_inductive(std::map<exprt, polynomialt> polynomials, patht &path);


Whitespace change

tautschnig · 2018-01-04T22:34:21Z

src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp

@@ -246,7 +246,7 @@ bool disjunctive_polynomial_accelerationt::accelerate(

  try
  {
-    path_is_monotone=utils.do_assumptions(polynomials, path, guard);
+    path_is_monotone = utils.do_assumptions(polynomials, path, guard);


Whitespace change

tautschnig · 2018-01-04T22:34:45Z

src/goto-instrument/accelerate/polynomial_accelerator.cpp

@@ -179,7 +179,7 @@ bool polynomial_acceleratort::accelerate(

  try
  {
-    path_is_monotone=utils.do_assumptions(polynomials, loop, guard);
+    path_is_monotone = utils.do_assumptions(polynomials, loop, guard);


Whitespace change

tautschnig · 2018-01-04T22:35:27Z

src/goto-instrument/accelerate/polynomial_accelerator.h

    const symbol_tablet &_symbol_table,
    const goto_functionst &_goto_functions,
-    exprt &_loop_counter)
+    const exprt &_loop_counter = nil_exprt())


What's this?

Default argument removing the need for 2 separate functions.

How is this related to this PR?

I was adding an extra constructor argument. In this case it was clunky, as there was a default parameter implemented manually, rather than using the language construct. I rolled that into one to reduce PR's size.

Ok, I would have preferred delegating constructors instead, out of some dislike for default arguments. But I guess I don't have solid facts to back this up. Just make sure the commit messages states includes a note about this refactoring.

The change has been separated into another commit.

LAJW · 2018-01-05T12:10:00Z

@peterschrammel I've noticed that intermediate commits no longer build. What's the point of splitting, if commits are not atomic?

LAJW · 2020-01-09T23:28:43Z

At this stage this has to be re-done. I don't want to argue about global state being bad. Closing.

tautschnig requested changes Oct 19, 2017

View reviewed changes

martin-cs requested changes Oct 19, 2017

View reviewed changes

allredj self-requested a review October 19, 2017 20:24

LAJW requested review from kroening, peterschrammel, romainbrenguier and thk123 as code owners October 20, 2017 17:14

tautschnig requested changes Oct 20, 2017

View reviewed changes

smowton approved these changes Oct 21, 2017

View reviewed changes

romainbrenguier approved these changes Oct 23, 2017

View reviewed changes

allredj approved these changes Oct 27, 2017

View reviewed changes

tautschnig reviewed Oct 27, 2017

View reviewed changes

peterschrammel requested changes Nov 10, 2017

View reviewed changes

LAJW requested a review from chrisr-diffblue as a code owner November 23, 2017 13:33

tautschnig assigned tautschnig, peterschrammel, martin-cs and LAJW Nov 30, 2017

peterschrammel requested changes Dec 2, 2017

View reviewed changes

peterschrammel mentioned this pull request Jan 4, 2018

Move solver factory into src/solvers to unify solver instantiation #1700

Closed

tautschnig reviewed Jan 4, 2018

View reviewed changes

Lukasz A.J. Wrona and others added 9 commits January 5, 2018 12:41

Refactor polynomial_acceleratort constructor

a14b4f7

Add random_var_freq and random_seed to propt

0eed1cc

Add random_var_freq and random_seed for minisat2 and glucose

10e2e66

Unify satchecker instantiation in cbmc_solvers

021a9eb

Unify satchecker instantiation in unit tests

069ec59

Clang format in string refinement

c619a13

Unify satchecker instantiation in solvers

5ba4887

Unify satchecker instantiation in goto-instrument

0aaee28

Register --random-var-freq and --random-seed command line options

a84b95d

tautschnig unassigned tautschnig and martin-cs Jan 7, 2018

LAJW changed the title ~~TG-925 Add command line options for setting up satcheck randomizer~~ [TG-925] Add command line options for setting up satcheck randomizer Mar 14, 2018

tautschnig mentioned this pull request Feb 8, 2019

Mini projects list update #4119

Merged

7 tasks

thk123 removed their request for review September 18, 2019 14:18

LAJW closed this Jan 9, 2020

LAJW deleted the sat-random branch January 9, 2020 23:28


		solver->prop().set_message_handler(get_message_handler());
		solver->set_prop(make_satcheck(options, use_simplifier, get_message_handler()));

		@@ -906,123 +913,178 @@ void cbmc_parse_optionst::help()

		std::cout << " * *\n";

		std::cout <<

[TG-925] Add command line options for setting up satcheck randomizer #1501

[TG-925] Add command line options for setting up satcheck randomizer #1501

Uh oh!

Conversation

LAJW commented Oct 19, 2017 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

LAJW commented Oct 19, 2017

Uh oh!

tautschnig left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

LAJW Oct 19, 2017 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

martin-cs commented Oct 19, 2017

Uh oh!

martin-cs left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

LAJW commented Oct 19, 2017 •

edited

Loading

LAJW Oct 19, 2017 •

edited

Loading

smowton commented Oct 20, 2017 •

edited

Loading