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

feat(main): handle check-sat-assuming statement

Browse source
This commit is contained in:
Simon Cruanes 2021-03-24 15:30:01 -04:00
parent 3fedca069d
commit 367c1945ef
4 changed files with 26 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/arith/base-term/Base_types.ml
View file

@ -146,7 +146,7 @@ type statement =
| Stmt_define of definition list
| Stmt_assert of term
| Stmt_assert_clause of term list
| Stmt_check_sat
| Stmt_check_sat of (bool * term) list
| Stmt_exit
let[@inline] term_equal_ (a:term) b = a==b
@ -1110,14 +1110,19 @@ module Statement = struct
| Stmt_define of definition list
| Stmt_assert of term
| Stmt_assert_clause of term list
| Stmt_check_sat
| Stmt_check_sat of (bool * term) list
| Stmt_exit
let pp out = function
| Stmt_set_logic s -> Fmt.fprintf out "(set-logic %s)" s
| Stmt_set_option l -> Fmt.fprintf out "(@[set-logic@ %a@])" (Util.pp_list Fmt.string) l
| Stmt_set_info (a,b) -> Fmt.fprintf out "(@[set-info@ %s@ %s@])" a b
| Stmt_check_sat -> Fmt.string out "(check-sat)"
| Stmt_check_sat [] -> Fmt.string out "(check-sat)"
| Stmt_check_sat l ->
let pp_pair out (b,t) =
if b then pp_term out t else Fmt.fprintf out "(@[not %a@])" pp_term t in
Fmt.fprintf out "(@[check-sat-assuming@ (@[%a@])@])"
(Fmt.list pp_pair) l
| Stmt_ty_decl (s,n) -> Fmt.fprintf out "(@[declare-sort@ %a %d@])" ID.pp s n
| Stmt_decl (id,args,ret) ->
Fmt.fprintf out "(@[<1>declare-fun@ %a (@[%a@])@ %a@])"

2
src/main/main.ml
View file

@ -111,7 +111,7 @@ module Dimacs = struct
(fun c ->
let lits = List.rev_map get_lit c in
stmts := Statement.Stmt_assert_clause lits :: !stmts);
stmts := Statement.Stmt_check_sat :: !stmts;
stmts := Statement.Stmt_check_sat [] :: !stmts;
Ok (List.rev !stmts))
with e ->
E.of_exn_trace e

7
src/smtlib/Process.ml
View file

@ -235,10 +235,13 @@ let process_stmt
| Statement.Stmt_exit ->
Log.debug 1 "exit";
raise Exit
| Statement.Stmt_check_sat ->
| Statement.Stmt_check_sat l ->
let assumptions =
List.map (fun (sign,t) -> Solver.mk_atom_t solver ~sign t) l
in
solve
?gc ?restarts ?dot_proof ~check ?pp_model ?time ?memory ?progress
~assumptions:[] ?hyps
~assumptions ?hyps
solver;
E.return()
| Statement.Stmt_ty_decl (id,n) ->

15
src/smtlib/Typecheck.ml
View file

@ -513,9 +513,18 @@ and conv_statement_aux ctx (stmt:PA.statement) : Stmt.t list =
let t = conv_term ctx t in
check_bool_ ctx t;
[Stmt.Stmt_assert t]
| PA.Stmt_check_sat -> [Stmt.Stmt_check_sat]
| PA.Stmt_check_sat_assuming _
| PA.Stmt_get_assertions
| PA.Stmt_check_sat -> [Stmt.Stmt_check_sat []]
| PA.Stmt_check_sat_assuming l ->
let l =
List.map
(fun (t,b) ->
let t = conv_term ctx (PA.const t) in
check_bool_ ctx t;
b,t)
l
in
[Stmt.Stmt_check_sat l]
| PA.Stmt_get_assertions
| PA.Stmt_get_option _
| PA.Stmt_get_info _
| PA.Stmt_get_model