simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 11:15:43 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

Update after Dolmen change

Browse source 
Dolmen Introduced a new 'Clause' statement, which has to be taken into
account in the test executable of msat.
This commit is contained in:
Guillaume Bury 2017-08-09 20:54:53 +02:00
parent 607ec3f043
commit 0119d04899
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/main.ml
View file

@ -73,6 +73,10 @@ module Make
match s.Dolmen.Statement.descr with match s.Dolmen.Statement.descr with
| Dolmen.Statement.Def (id, t) -> T.def id t | Dolmen.Statement.Def (id, t) -> T.def id t
| Dolmen.Statement.Decl (id, t) -> T.decl id t | Dolmen.Statement.Decl (id, t) -> T.decl id t
| Dolmen.Statement.Clause l ->
let cnf = T.antecedent (Dolmen.Term.or_ l) in
hyps := cnf @ !hyps;
S.assume cnf
| Dolmen.Statement.Consequent t -> | Dolmen.Statement.Consequent t ->
let cnf = T.consequent t in let cnf = T.consequent t in
hyps := cnf @ !hyps; hyps := cnf @ !hyps;