reintegrate msat directly in-tree #11

c-cube · 2021-07-18T13:29:19Z

benefits:

remove mcsat code
ability to modify more easily
one fewer dep to synchronize on

- 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

it's part of the actions provided to the theory. close #19

feat: allow to set the default polarity of variables at creation time

feat: allow the theory to ask for some literals to be decided on

breaking change for `solve`, remove the `on_conflict` callback. it's provided at creation time instead.

c-cube and others added 30 commits December 30, 2017 21:10

fix small linter issue in opam

a9d7626

Added ICFP presentation in README

c8321b4

Merge branch 'master' of github.com:Gbury/mSAT

14c92bb

New shiny travis script + test dep on dolmen.dev

8821b77

Typo in travis.yml

25b8c97

[travis] Force installation of dev version

16e6be0

Merge branch 'master' of github.com:Gbury/mSAT

7cd541b

Fix typo in opam file

fd75f53

[travis] Fix faulty conditional for dolmen pinning

696002b

Fix typo in doc

1722730

Fix typo in the pigeon hole test description

0425ce6

Add assertion to check theory conflict clauses

354f201

Propagate consequences at the lowest level possible

a5eeaa0

Merge branch 'master' of github.com:Gbury/mSAT

8cdfe65

Prevent semantic propagations at level 0

2bba885

Bugfix for user lvl push when already unsat

5e57bfc

Update for latest version of dolmen

4bb1f5b

capitalization of files; add new Log

48ec2d7

big refactoring

768f59f

- 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

f64a155

move tseitin transformation into its own lib

2707215

fix warnings

ec7fa9e

update travis

a978ec9

travis

cb45782

cleanup in fields

d9ceba7

update opam files

f5b4f5d

remove useless dir

b92d8b3

ocpindent config

2b1bef9

makefile

797e1b8

use generative functors, remove a layer of nesting for SMT libs

cbe3750

c-cube added 29 commits September 8, 2020 22:43

fix: support containers 2.8.1 and above

8eb32fa

fix test on 2.8.1

9ef84f1

prepare for 0.8.3

4bce0f3

feat: allow to set the default polarity of variables at creation time

d9bf16d

feat: allow the theory to ask for some literals to be decided on

79b1585

it's part of the actions provided to the theory. close #19

fix: in final-check, resume if there are new decisions to do

2286a72

fix: only push atoms that don't have a value into next_decisions

919c1e6

refactor: account for @Gbury's review

4097ed9

feat: pass a sign along with the formula in acts_add_decision_lit

764695b

Merge pull request #24 from Gbury/feat-lit-pol

d3103c5

feat: allow to set the default polarity of variables at creation time

Merge pull request #22 from Gbury/feat-th-decisions

a3e618a

feat: allow the theory to ask for some literals to be decided on

prepare for 0.9

14e07f7

typo

6df3516

feat: add on_conflict callback

a64202c

fix: termination issue when using add_decision_lit

db042f7

prepare for 0.9.1

457aa15

merge opam fix from opam-repo

b6ea55e

callbacks for conflict/decisions/new-atoms

941fe92

breaking change for `solve`, remove the `on_conflict` callback. it's provided at creation time instead.

prepare for vendoring

d024a6a

vendor current msat in src/sat for further modifications

1a58ab0

cleanup msat

4a337a8

cleanup msat, rename it sidekick.sat

564dcec

wip: remove all traces of mcsat from src/sat

4cb8887

use a pure sat solver for cnf files

1aa160f

chore: try to build again

5faa1d6

chore: CI on PRs

ff5cf12

feat: optional memtrace support

c7bf4b0

feat: make mtime optional with dummy "tef" backend

041e831

refactor(sat): use first-class modules instead of records

15d86d7

c-cube merged commit cab541e into master Jul 19, 2021

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

reintegrate msat directly in-tree #11

reintegrate msat directly in-tree #11

c-cube commented Jul 18, 2021

reintegrate msat directly in-tree #11

reintegrate msat directly in-tree #11

Conversation

c-cube commented Jul 18, 2021