mirror of
https://github.com/AdaCore/cvc5.git
synced 2026-02-12 12:32:16 -08:00
fd0df78ad4
Includes several fixes found during testing: A check to avoid assertion failure in the flex parser Changes atomic SEXPR to symbols instead of constant strings to avoid spurious error messages for non-standard characters Changes to options configuration for Flex for performance (as a result, this does not fix check-synth doesn't flush output #9257). Fix for --stdin-input-per-line to not set incremental by default for non-interactive inputs. Note that TPTP parsing still uses the ANTLR parser. Fixes #9258. Fixes #8374. Fixes #1862. Fixes #791. Fixes cvc5/cvc5-wishues#142.
96 lines
2.4 KiB
Python
96 lines
2.4 KiB
Python
#!/usr/bin/env python3
|
|
###############################################################################
|
|
# Top contributors (to current version):
|
|
# Andrew V. Jones, Mathias Preiner, Aina Niemetz
|
|
#
|
|
# This file is part of the cvc5 project.
|
|
#
|
|
# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS
|
|
# in the top-level source directory and their institutional affiliations.
|
|
# All rights reserved. See the file COPYING in the top-level source
|
|
# directory for licensing information.
|
|
# #############################################################################
|
|
#
|
|
# A simple test file to interact with cvc5 with line editing
|
|
##
|
|
|
|
import sys
|
|
import pexpect
|
|
|
|
def check_iteractive_shell():
|
|
"""
|
|
Interacts with cvc5's interactive shell and checks that things such a tab
|
|
completion and "pressing up" works.
|
|
"""
|
|
|
|
# Open cvc5
|
|
child = pexpect.spawnu("bin/cvc5", timeout=1)
|
|
|
|
# We expect to see the cvc5 prompt
|
|
child.expect("cvc5>")
|
|
|
|
# If we send a line with just 'BOOLE' ...
|
|
child.sendline("(set-log")
|
|
|
|
# ... then we get an error
|
|
child.expect("Expected SMT-LIBv2 command.")
|
|
|
|
# Start sending 'BOOL' (without an E)
|
|
child.send("(declare-data")
|
|
|
|
# Send tab twice
|
|
child.sendcontrol("i")
|
|
child.sendcontrol("i")
|
|
|
|
# We expect to see the completion
|
|
child.expect("declare-datatype.*declare-datatypes")
|
|
|
|
# NOTE: the double tab has completed our '(declare-data' to '(declare-datatype'!
|
|
|
|
# Now send enter (which submits '(declare-datatype')
|
|
child.send(")")
|
|
child.sendcontrol("m")
|
|
|
|
# So we expect to see an error for 'BOOLE'
|
|
child.expect("Expected SMT-LIBv2 symbol")
|
|
|
|
# Send enter
|
|
child.sendcontrol("m")
|
|
|
|
# We expect to see the cvc5 prompt
|
|
child.expect("cvc5>")
|
|
|
|
# Now send an up key
|
|
child.send("\033[A")
|
|
|
|
# Send enter
|
|
child.sendcontrol("m")
|
|
|
|
# We expect to see the previous error again
|
|
child.expect("Expected SMT-LIBv2 symbol")
|
|
|
|
return 0
|
|
|
|
|
|
def main():
|
|
"""
|
|
Runs our interactive shell test
|
|
|
|
Caveats:
|
|
|
|
* If we don't have the "pexpect" model, the test doesn't get run, but
|
|
passes
|
|
|
|
* We expect pexpect to raise and exit with a non-zero exit code if any
|
|
of the steps fail
|
|
"""
|
|
|
|
# If any of the "steps" fail, the pexpect will raise a Python will exit
|
|
# with a non-zero error code
|
|
sys.exit(check_iteractive_shell())
|
|
|
|
if __name__ == "__main__":
|
|
main()
|
|
|
|
# EOF
|