Add mkInteger to the API (#5274)
authormudathirmahgoub <mudathirmahgoub@gmail.com>
Thu, 29 Oct 2020 18:26:51 +0000 (13:26 -0500)
committerGitHub <noreply@github.com>
Thu, 29 Oct 2020 18:26:51 +0000 (13:26 -0500)
commitd23ba1433846b9baaf6149137aa999c1af60c516
treeb75389566b726edcaf32cb0f8ab2059bba9e1528
parent6898ab93a3858e78b20af38e537fe48ee9140c58
Add mkInteger to the API (#5274)

This PR adds mkInteger to the API and update mkReal to ensure that the returned term has real sort.
The parsers are modified to parse numbers like "0" "5" as integers and "0.0" and "15.0" as reals.
This means subtyping is effectively eliminated from all theories except arithmetic.
Other changes:

Term::isValue is removed which was introduced to support parsing for constant arrays. It is no longer needed after this PR.
Benchmarks are updated to match the changes in the parsers
Co-authored-by: Andrew Reynolds andrew-reynolds@uiowa.edu
45 files changed:
examples/api/combination.cpp
examples/api/datatypes.cpp
examples/api/linear_arith.cpp
examples/api/python/combination.py
examples/api/python/datatypes.py
examples/api/python/linear_arith.py
examples/api/python/sequences.py
examples/api/python/sets.py
examples/api/python/strings.py
examples/api/python/sygus-fun.py
examples/api/python/sygus-grammar.py
examples/api/python/sygus-inv.py
examples/api/sequences.cpp
examples/api/sets.cpp
examples/api/strings.cpp
examples/api/sygus-fun.cpp
examples/api/sygus-grammar.cpp
examples/api/sygus-inv.cpp
examples/simple_vc_cxx.cpp
examples/simple_vc_quant_cxx.cpp
src/api/cvc4cpp.cpp
src/api/cvc4cpp.h
src/api/python/cvc4.pxd
src/api/python/cvc4.pxi
src/expr/array_store_all.cpp
src/parser/cvc/Cvc.g
src/parser/smt2/Smt2.g
src/parser/smt2/smt2.cpp
src/parser/tptp/Tptp.g
src/printer/cvc/cvc_printer.cpp
src/printer/smt2/smt2_printer.cpp
src/theory/arith/arith_rewriter.cpp
src/theory/arith/kinds
src/theory/arith/theory_arith_type_rules.h
test/api/reset_assertions.cpp
test/api/sep_log_api.cpp
test/regress/regress0/get-value-reals-ints.smt2
test/regress/regress0/get-value-reals.smt2
test/unit/api/grammar_black.h
test/unit/api/python/test_grammar.py
test/unit/api/python/test_term.py
test/unit/api/python/test_to_python_obj.py
test/unit/api/solver_black.h
test/unit/api/term_black.h
test/unit/theory/theory_sets_type_rules_white.h