Simon Cruanes
6762985d18
expose {push,pop} in main solver
2019-02-11 16:55:43 +01:00
Simon Cruanes
241e2fa4d7
remove useless functions
2019-02-11 16:55:43 +01:00
Simon Cruanes
87fc9aef26
reinstate better way of picking watch literals
2019-02-11 16:55:43 +01:00
Simon Cruanes
5279456419
reset some record accesses, for perf
2019-02-11 16:55:43 +01:00
Simon Cruanes
b2e646343a
do not expose St in solver, but only expose a restricted API.
2019-02-11 16:55:43 +01:00
Simon Cruanes
a612a1cda2
make Solver.t more lightweight by removing some useless fields
2019-02-11 16:55:43 +01:00
Simon Cruanes
a34c191ddc
add optional size argument to create functions
2019-02-11 16:55:43 +01:00
Simon Cruanes
ef7333af6d
make state explicit and add type t state-wrapper in most modules
2019-02-11 16:55:43 +01:00
Simon Cruanes
eff3f8024f
wip: use submodules of Solver_types to clean up code
2019-02-11 16:55:43 +01:00
Simon Cruanes
8eef2deebd
faster addition of clauses' watch literals
...
instead of sorting the whole clause, just select two highest level lits
2019-02-11 16:55:43 +01:00
Simon Cruanes
9bc85160b8
restrict what Msat core lib exposes, provide shortcuts
2019-02-11 16:55:43 +01:00
Simon Cruanes
cbe3750b0d
use generative functors, remove a layer of nesting for SMT libs
2019-02-11 16:55:43 +01:00
Simon Cruanes
d9ceba72d4
cleanup in fields
2019-02-11 16:55:43 +01:00
Simon Cruanes
2707215aa2
move tseitin transformation into its own lib
2019-02-11 16:55:43 +01:00
Simon Cruanes
768f59f88b
big refactoring
...
- 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
2019-02-11 16:55:43 +01:00
Simon Cruanes
48ec2d732c
capitalization of files; add new Log
2019-02-11 16:55:43 +01:00
Guillaume Bury
5e57bfc827
Bugfix for user lvl push when already unsat
2018-09-11 14:19:22 +02:00
Guillaume Bury
2bba885266
Prevent semantic propagations at level 0
2018-07-24 23:42:20 +02:00
Guillaume Bury
a5eeaa0edc
Propagate consequences at the lowest level possible
2018-07-24 21:57:12 +02:00
Guillaume Bury
354f2013b1
Add assertion to check theory conflict clauses
2018-07-24 21:56:58 +02:00
Guillaume Bury
1722730e26
Fix typo in doc
2018-04-18 11:53:55 +02:00
Guillaume Bury
bed469c0cf
Clear unused hyps in coq proofs
2017-08-29 15:18:10 +02:00
Guillaume Bury
7749f7aaac
Manual re-indent
2017-08-25 19:15:12 +02:00
Guillaume Bury
679d928b88
Auto re-indent
2017-08-25 19:11:58 +02:00
Guillaume Bury
4989026f06
Fix mcsat conflict analysis
...
When analyzing an mcst conflict clause and looking at a semantic
propagation in the trail, the last resolved clause was looked at again,
which caused an invalid history to be generated (the computation of the
backtrack clause was not affected because the second resolution of the clause
was basically a no-op thanks to the 'seen' field), thus it did not
introduce any soundness bug, just a faulty clause history which was
caught during proof expansion.
2017-08-25 18:33:42 +02:00
Guillaume Bury
607ec3f043
Added Coq backend (not tested yet)
2017-08-09 09:45:18 +02:00
Guillaume Bury
0c99e6b2e7
[breaking] Better interface for the DOT backend
2017-07-20 13:55:55 +02:00
Guillaume Bury
92835bcdda
Add useful function on proof steps
...
These new functions are designed to help people if (or when) the proof
API will break next time (i.e. adding a new variant case in step).
2017-04-12 20:48:08 +02:00
Guillaume Bury
88c122c4a4
Remove incorrect tag duplication
2017-04-12 19:40:21 +02:00
Guillaume Bury
0fe8ded071
[bugfix] Fix typo following doublon elimination
...
Following a bugfix for doublon elimination, doublons are now eliminated
in add_clause, and as such, in case no simplification is made, the
clause without doublons should be used (and not init). This was a typo
missed during the refactoring of doublon elimination.
2017-04-12 19:23:46 +02:00
Guillaume Bury
7e95911dd8
[bugfix] Allow late mcsat conflicts (wrt assigns)
2017-04-07 15:13:27 +02:00
Guillaume Bury
5725cf5173
Move calls to eliminate_doublons in a single place
2017-03-31 15:39:43 +02:00
Guillaume Bury
f5f9a4ab69
Extend the 'seen' field to store more information
2017-03-31 15:17:51 +02:00
Guillaume Bury
88eaa03968
Internal check also checks for undecided lits
2017-03-30 19:29:53 +02:00
Guillaume Bury
2874dd9cea
[bugfix] Fix undecided lit bug
2017-03-30 18:47:54 +02:00
Guillaume Bury
154cb373fc
Add generativity of Dimacs functor
...
Since the dimacs functor has an internal state (relating to the output
in iCNF format), it is desirable to have a generative functor, inc as
esomeone wants to output select parts of a problem to two distinct iCNF
files).
2017-03-27 16:32:25 +02:00
Guillaume Bury
d0d47fe73f
Moved Dimacs problem export in its own module
2017-03-27 15:37:41 +02:00
Guillaume Bury
7776b6e2f0
Fix use of asprintf (missing in 4.00.1)
2017-02-15 14:03:10 +01:00
Guillaume Bury
a13906184c
Fix warnings
2017-02-15 13:34:21 +01:00
Guillaume Bury
8076c06047
[bugfix] Eliminate duplicates in input clauses
...
When adding clauses that conatins duplicates, the checking
of some proof would fail because there would sometime be multiple
littrals to resolve over. This fixes that problem.
2017-02-15 13:04:54 +01:00
Guillaume Bury
8acf02cb74
[bugfix] subterm insertion in forgetful propagation
2017-01-29 13:38:00 +01:00
Guillaume Bury
44509c6f8d
[bugfix] conflict in forgetful propagation
2017-01-27 17:56:47 +01:00
Guillaume Bury
928622b511
[feature] New functions new_lit and new_atom
2017-01-24 11:12:17 +01:00
Guillaume Bury
204e184b86
[doc] Better description for Plugin_intf.reason
2017-01-24 11:12:17 +01:00
Guillaume Bury
1f5b5fc422
Renamed new_atom -> create_atom
2017-01-24 11:12:17 +01:00
Guillaume Bury
d538e19411
Fix typo of Plugin_intf.reason
2017-01-17 15:59:29 +01:00
Guillaume Bury
ea2c905644
Add forgetful propagation
2017-01-17 13:16:00 +01:00
Guillaume Bury
e8e619f3c7
Do not decide on unused variables
2017-01-17 12:29:39 +01:00
Guillaume Bury
c77c997ab8
Add used field to variables
2017-01-17 12:26:18 +01:00
Guillaume Bury
b5d816fbac
Typo in doc
2017-01-17 12:26:12 +01:00
