Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
a69faf28
Commit
a69faf28
authored
May 18, 2015
by
David Hauzar
Browse files
Change the names of parse_cvc4_z3_model* to Parse_smtv2_model*.
parent
e56b8f56
Changes
7
Hide whitespace changes
Inline
Side-by-side
Makefile.in
View file @
a69faf28
...
...
@@ -133,8 +133,8 @@ LIBGENERATED = src/util/config.ml \
src/parser/parser.mli src/parser/parser.ml
\
src/driver/driver_parser.mli src/driver/driver_parser.ml
\
src/driver/driver_lexer.ml
\
src/driver/parse_
cvc4_z3
_model_parser.mli src/driver/parse_
cvc4_z3
_model_parser.ml
\
src/driver/parse_
cvc4_z3
_model_lexer.ml
\
src/driver/parse_
smtv2
_model_parser.mli src/driver/parse_
smtv2
_model_parser.ml
\
src/driver/parse_
smtv2
_model_lexer.ml
\
src/session/compress.ml src/session/xml.ml
\
src/session/strategy_parser.ml
\
lib/ocaml/why3__BigInt_compat.ml
...
...
@@ -149,7 +149,7 @@ LIB_CORE = ident ty term pattern decl theory \
LIB_DRIVER
=
call_provers driver_ast driver_parser driver_lexer driver
\
whyconf autodetection
\
parse_
cvc4_z3
_model_parser parse_
cvc4_z3
_model_lexer parse_
cvc4_z3
_model
parse_
smtv2
_model_parser parse_
smtv2
_model_lexer parse_
smtv2
_model
LIB_MLW
=
ity
expr
dexpr
...
...
drivers/cvc4_15.drv
View file @
a69faf28
...
...
@@ -24,7 +24,7 @@ transformation "introduce_premises"
transformation "intro_projections_counterexmp"
(* Counterexamples: set model parser *)
model_parser "
cvc4_z3
"
model_parser "
smtv2
"
import "smt-libv2.drv"
import "smt-libv2-bv.gen"
...
...
drivers/cvc4_bare.drv
View file @
a69faf28
...
...
@@ -20,7 +20,7 @@ prelude "(set-option :produce-models true)"
transformation "introduce_premises"
(* Counterexamples: set model parser *)
model_parser "
cvc4_z3
"
model_parser "
smtv2
"
import "smt-libv2.drv"
...
...
drivers/z3_432.drv
View file @
a69faf28
...
...
@@ -13,7 +13,7 @@ transformation "introduce_premises"
transformation "intro_projections_counterexmp"
(* Counterexamples: set model parser *)
model_parser "
cvc4_z3
"
model_parser "
smtv2
"
import "smt-libv2.drv"
...
...
src/driver/parse_
cvc4_z3
_model.ml
→
src/driver/parse_
smtv2
_model.ml
View file @
a69faf28
...
...
@@ -17,7 +17,7 @@ open Term
open
Model_parser
open
Lexing
let
debug
=
Debug
.
register_info_flag
"parse_
cvc4_z3
_model"
let
debug
=
Debug
.
register_info_flag
"parse_
smtv2
_model"
~
desc
:
"Print@ debugging@ messages@ about@ parsing@ model@ \
returned@ from@ cvc4@ or@ z3."
...
...
@@ -88,14 +88,14 @@ let get_position lexbuf =
let
do_parsing
model
=
let
lexbuf
=
Lexing
.
from_string
model
in
try
Parse_
cvc4_z3
_model_parser
.
output
Parse_
cvc4_z3
_model_lexer
.
token
lexbuf
Parse_
smtv2
_model_parser
.
output
Parse_
smtv2
_model_lexer
.
token
lexbuf
with
|
Parse_
cvc4_z3
_model_lexer
.
SyntaxError
->
|
Parse_
smtv2
_model_lexer
.
SyntaxError
->
Warning
.
emit
~
loc
:
(
get_position
lexbuf
)
"Error@ during@ lexing@ of@ smtlib@ model:@ unexpected character"
;
[]
|
Parse_
cvc4_z3
_model_parser
.
Error
->
|
Parse_
smtv2
_model_parser
.
Error
->
begin
let
loc
=
get_position
lexbuf
in
Warning
.
emit
~
loc
:
loc
"Error@ during@ parsing@ of@ smtlib@ model"
;
...
...
@@ -121,5 +121,5 @@ let parse input printer_mapping =
|
Not_found
->
[]
let
()
=
register_model_parser
"
cvc4_z3
"
parse
let
()
=
register_model_parser
"
smtv2
"
parse
~
desc
:
"Parser@ for@ the@ model@ of@ cv4@ and@ z3."
src/driver/parse_
cvc4_z3
_model_lexer.mll
→
src/driver/parse_
smtv2
_model_lexer.mll
View file @
a69faf28
{
open
Parse_
cvc4_z3
_model_parser
open
Parse_
smtv2
_model_parser
exception
SyntaxError
}
...
...
src/driver/parse_
cvc4_z3
_model_parser.mly
→
src/driver/parse_
smtv2
_model_parser.mly
View file @
a69faf28
...
...
@@ -104,3 +104,4 @@ array:
array_skipped_part
:
|
LPAREN
term_list
RPAREN
{}
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment