[wip] major refactoring for perf and modularity #11

c-cube · 2017-12-28T13:08:48Z

move to ~~jbuilder~~ dune
style stuff
migrate to 4.03
cut into small sub-libraries
use sequence
make state explicit, remove stateful functors
heavy perf improvements
remove smt-related libs
add sudoku solver to test the functor
remove push/pop, replaced by faster assumptions-powered unsat-core

Gbury · 2017-12-28T13:17:06Z

Looks good (as long as the Travis check pass). Is there a reason for having filenames capitalized ? I usually keep all my folders/filenames lowcase because it's easier to type in the terminal (but it's not an absolute rule).

Gbury · 2017-12-28T13:21:31Z

Travis configuration and opam file should be updated to reflect the changes in ocaml versions

c-cube · 2017-12-28T13:28:36Z

I use capitalized file names these days, because it maps exactly to the module name. When using acronyms, if avoids having files named cNF.ml.

c-cube · 2017-12-28T15:08:31Z

Questions:

why, in External, is solve calling pop then push? If there were local assumptions they will be lost…
should we move all the test stuff into a new library msmt, with corresponding opam file? or is it just hidden?
- if so, should we have a proper internal AST with hashconsing (I have several of those already)?

Gbury · 2017-12-29T16:57:25Z

In External, since the functions returned in the sat_state and unsat_state use the mutable state of the solver, if you pop after solving, these function will not work anymore. The curreent approach is correct because there are really only two states the solver should be in when using external:

nothing happened, the solver is at level 0, thus popping does not do anything
External.solve has been called previously, which left exactly one level of local assumptions to be popped.
The assumption was that a user of External wouldn't use functions from Internal that could change the state of the solver. If you find a way to make it work without this assumption then all the better, that that would probably require some additional state to be remembered.

The test stuff is currently hidden (and ideally not part of what is installed), but it could indeed be moved to a separate library. I didn't make it visible because I felt the code wasn't really good enough, but feel free to improve it.

c-cube · 2017-12-30T18:41:08Z

I think the major changes are there. You might want to start by looking at the API changes, and if it's ok, then look into the code itself.

Note that in mc2 there are still some parts that I consider more elegant:

the separation between values and terms
conflict analysis: https://github.com/c-cube/mc2/blob/6f77e4f346fb676b262a4be194543958e61b278b/src/core/Internal.ml#L788 and below
most of the proof post-processing (and types): https://github.com/c-cube/mc2/blob/6f77e4f346fb676b262a4be194543958e61b278b/src/core/Proof.ml

timothee-haudebourg · 2018-05-25T09:36:06Z

You have a msat.exe file that appeared and I don't think its supposed to be there.

c-cube · 2018-05-25T14:52:09Z

The msat.exe is convenient for running msat, is all.

Otherwise: this PR is a bit old, another pass might be useful to get it ready ot be merged I think.

Gbury · 2018-05-25T14:54:22Z

I'll try and do a serious review soon (as in in a few days, one week max). @c-cube do you think you'll have some time to address the potential comments ?

c-cube · 2018-05-25T15:28:30Z

I think so, yes. I'm spending too much time on my own fork (sidekick) but well.

c-cube · 2018-05-31T00:49:18Z

rebased

c-cube · 2018-05-31T01:22:00Z

Ugh, I hate travis -_-

- move to jbuilder - use a functorial heap (with indices embedded in lit/var) - update Vec with optims from mc2 - change semantics of Vec.shrink - use new Log module

this replaces the old "tag" system

- goal: do not keep clauses alive after they're gc'd - default is to indeed log proofs

more accurate representation of the semantics, esp. for theory lemmas

Gbury

Looks very good overall ! Some small comments here and there, but this is already mergeable, and we can fix things later.

Last question: why is Backtrackable_ref part of core and not sudoku ? It seems to only be used in the sudoku example, and even though it is very convenient for SMT solvers, I don't know if it really needs to be part of the core of msat.

src/core/Internal.ml

Gbury · 2017-12-29T17:30:27Z

src/core/Internal.ml

+  (* inverse of the activity factor for variables. Default 1/0.999 *)
+
+  let clause_decay : float = 1. /. 0.999
+  (* inverse of the activity factor for clauses. Default 1/0.95 *)


Defaults values in the comments are out of sync for var_decay and clause_decay.

src/core/Solver_types_intf.ml

src/core/Vec.mli

src/core/Internal.ml

Gbury · 2019-02-04T22:39:10Z

src/backend/Dimacs.ml

-      ) hyps);
+  let export st fmt ~hyps ~history ~local =
+    assert false
+    (* FIXME


Why is this commented out ? I mean, did you encounter some example that made the assertions fail ?

it's because the vecs have changed, and stuff was hidden (in particular, the premises, I think).

edit: clauses are not stored as faithfully now (no more local assumptions, no storage of unit hypothesis, etc.) so this makes less sense imho

Gbury · 2019-02-04T22:40:17Z

src/backend/Dimacs.ml

-      ) hyps);
+    assert false
+    (* FIXME
+    assert (Vec.for_all (fun c -> St.Clause.premise c = St.Hyp) hyps);


Same question. Do the changes to clauses require these functions to be changed significantly ?

- use `cid` instead of `name` for clauses - has the name of the clause, not its content - simplified some things

This reverts commit 5d7e345.

c-cube · 2019-02-11T15:58:31Z

🎉 🎉 🎉 🌮 🎆

c-cube requested a review from Gbury December 28, 2017 13:08

c-cube self-assigned this Dec 28, 2017

c-cube added the enhancement label Dec 28, 2017

c-cube force-pushed the wip-refactor branch from fbc893b to 2a3afe7 Compare December 28, 2017 15:29

c-cube added this to the 1.0 milestone Dec 28, 2017

Gbury mentioned this pull request May 25, 2018

use non generative api #12

Closed

c-cube force-pushed the wip-refactor branch from 7324647 to 60e27c3 Compare May 31, 2018 00:39

c-cube added 11 commits October 23, 2018 19:47

capitalization of files; add new Log

3a04d17

big refactoring

8bdb511

- move to jbuilder - use a functorial heap (with indices embedded in lit/var) - update Vec with optims from mc2 - change semantics of Vec.shrink - use new Log module

details

1d9f52f

move tseitin transformation into its own lib

12ae2fc

fix warnings

45d3f2e

update travis

fe11624

travis

a5f48d0

cleanup in fields

710ccc4

update opam files

4df62d4

remove useless dir

0c676b4

ocpindent config

5394b4b

c-cube added 13 commits January 28, 2019 19:21

api: sat_state takes formulas, not atoms

62f4a26

api: remove spurious () for calls to solve

2a960be

api: annotate input clauses with theory proofs, too

f936b55

this replaces the old "tag" system

chore: be robust to deprecations

104f036

feat: allow optional disabling of proof logging

b603f72

- goal: do not keep clauses alive after they're gc'd - default is to indeed log proofs

refactor: rename flag clause.{learnt,removable}

43edf4d

more accurate representation of the semantics, esp. for theory lemmas

rename log-proof to store-proof

ded7955

feat: expose eval_atom

d21e914

feat: expose printers

13b3240

fix: when simplifying, copy flags properly

103b480

refactor: cleaner choice of which vector to add a clause to

b9653bf

test: use mdx to ensure the readme code snippets compile

dd366f6

fix: msat.tseitin depends on msat

d9ecd9b

c-cube force-pushed the wip-refactor branch from 042a515 to d9ecd9b Compare February 3, 2019 01:10

c-cube added 2 commits February 2, 2019 19:28

doc: check something in the readme

60a6f7b

doc: add a section and test on the sudoku solver

9c75f66

Gbury approved these changes Feb 4, 2019

View reviewed changes

c-cube added 9 commits February 4, 2019 20:35

refactor: fix problems from review

14aa139

- use `cid` instead of `name` for clauses - has the name of the clause, not its content - simplified some things

refactor: move Backtrackable_ref into its own sub-library

8c8c7b4

fix(propagate): insert propagated literal itself

06cebf9

refactor: a bit of cleanup for mcsat

beaf730

detail: add debug message

992609c

feat: re-export exn

508e513

refactor: return an array from conflict analysis

b3575ae

fix: catch E_unsat in assume, if one adds an empty clause

5d7e345

Revert "fix: catch E_unsat in assume, if one adds an empty clause"

403026b

This reverts commit 5d7e345.

Gbury merged commit 4127db2 into master Feb 11, 2019

This was referenced Feb 14, 2019

design clean API for theories #13

Closed

Improve performances #8

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[wip] major refactoring for perf and modularity #11

[wip] major refactoring for perf and modularity #11

c-cube commented Dec 28, 2017 •

edited

Loading

Gbury commented Dec 28, 2017

Gbury commented Dec 28, 2017

c-cube commented Dec 28, 2017

c-cube commented Dec 28, 2017

Gbury commented Dec 29, 2017

c-cube commented Dec 30, 2017

timothee-haudebourg commented May 25, 2018

c-cube commented May 25, 2018

Gbury commented May 25, 2018

c-cube commented May 25, 2018

c-cube commented May 31, 2018

c-cube commented May 31, 2018

Gbury left a comment

Gbury Dec 29, 2017

Gbury Feb 4, 2019

c-cube Feb 5, 2019 •

edited

Loading

Gbury Feb 4, 2019

c-cube commented Feb 11, 2019

[wip] major refactoring for perf and modularity #11

[wip] major refactoring for perf and modularity #11

Conversation

c-cube commented Dec 28, 2017 • edited Loading

Gbury commented Dec 28, 2017

Gbury commented Dec 28, 2017

c-cube commented Dec 28, 2017

c-cube commented Dec 28, 2017

Gbury commented Dec 29, 2017

c-cube commented Dec 30, 2017

timothee-haudebourg commented May 25, 2018

c-cube commented May 25, 2018

Gbury commented May 25, 2018

c-cube commented May 25, 2018

c-cube commented May 31, 2018

c-cube commented May 31, 2018

Gbury left a comment

Choose a reason for hiding this comment

Gbury Dec 29, 2017

Choose a reason for hiding this comment

Gbury Feb 4, 2019

Choose a reason for hiding this comment

c-cube Feb 5, 2019 • edited Loading

Choose a reason for hiding this comment

Gbury Feb 4, 2019

Choose a reason for hiding this comment

c-cube commented Feb 11, 2019

c-cube commented Dec 28, 2017 •

edited

Loading

c-cube Feb 5, 2019 •

edited

Loading