git.libre-soc.org Git - cvc5.git/commit

author	Aina Niemetz <aina.niemetz@gmail.com>
	Wed, 1 Apr 2020 01:12:16 +0000 (18:12 -0700)
committer	GitHub <noreply@github.com>
	Wed, 1 Apr 2020 01:12:16 +0000 (18:12 -0700)
commit	cfeaf40ed6a9d4d7fec925352e30d2470a1ca567
tree	e69411603787d99cea12d729ec0a0a2ae8889f20	tree
parent	186b3872a3de454d0f30224dc2e0a396163c3fdc	commit \| diff

Rename checkValid/query to checkEntailed. (#4191)

This renames api::Solver::checkValidAssuming to checkEntailed and
removes api::Solver::checkValid. Internally, SmtEngine::query is renamed
to SmtEngine::checkEntailed, and these changes are further propagated to
the Result class.

268 files changed:

examples/SimpleVC.java		diff \| blob \| history
examples/SimpleVC.ml		diff \| blob \| history
examples/SimpleVC.php		diff \| blob \| history
examples/SimpleVC.pl		diff \| blob \| history
examples/SimpleVC.py		diff \| blob \| history
examples/SimpleVC.rb		diff \| blob \| history
examples/SimpleVC.tcl		diff \| blob \| history
examples/api/bitvectors-new.cpp		diff \| blob \| history
examples/api/bitvectors.cpp		diff \| blob \| history
examples/api/combination-new.cpp		diff \| blob \| history
examples/api/combination.cpp		diff \| blob \| history
examples/api/extract-new.cpp		diff \| blob \| history
examples/api/extract.cpp		diff \| blob \| history
examples/api/helloworld-new.cpp		diff \| blob \| history
examples/api/helloworld.cpp		diff \| blob \| history
examples/api/java/BitVectors.java		diff \| blob \| history
examples/api/java/Combination.java		diff \| blob \| history
examples/api/java/HelloWorld.java		diff \| blob \| history
examples/api/java/LinearArith.java		diff \| blob \| history
examples/api/linear_arith-new.cpp		diff \| blob \| history
examples/api/linear_arith.cpp		diff \| blob \| history
examples/api/python/bitvectors.py		diff \| blob \| history
examples/api/python/combination.py		diff \| blob \| history
examples/api/python/extract.py		diff \| blob \| history
examples/api/python/helloworld.py		diff \| blob \| history
examples/api/python/linear_arith.py		diff \| blob \| history
examples/api/python/sets.py		diff \| blob \| history
examples/api/sets-new.cpp		diff \| blob \| history
examples/api/sets.cpp		diff \| blob \| history
examples/simple_vc_cxx.cpp		diff \| blob \| history
src/api/cvc4cpp.cpp		diff \| blob \| history
src/api/cvc4cpp.h		diff \| blob \| history
src/api/python/cvc4.pxd		diff \| blob \| history
src/api/python/cvc4.pxi		diff \| blob \| history
src/smt/command.cpp		diff \| blob \| history
src/smt/smt_engine.cpp		diff \| blob \| history
src/smt/smt_engine.h		diff \| blob \| history
src/util/result.cpp		diff \| blob \| history
src/util/result.h		diff \| blob \| history
src/util/result.i		diff \| blob \| history
test/regress/regress0/arith/arith.01.cvc		diff \| blob \| history
test/regress/regress0/arith/arith.02.cvc		diff \| blob \| history
test/regress/regress0/arith/arith.03.cvc		diff \| blob \| history
test/regress/regress0/arith/bug549.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-014.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-015.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-021.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-023.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-025.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-042.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-042.min.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-079.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-interval.cvc		diff \| blob \| history
test/regress/regress0/boolean-prec.cvc		diff \| blob \| history
test/regress/regress0/bug310.cvc		diff \| blob \| history
test/regress/regress0/bug32.cvc		diff \| blob \| history
test/regress/regress0/bug322b.cvc		diff \| blob \| history
test/regress/regress0/bug486.cvc		diff \| blob \| history
test/regress/regress0/bv/bvcomp.cvc		diff \| blob \| history
test/regress/regress0/bv/bvsimple.cvc		diff \| blob \| history
test/regress/regress0/cvc-rerror-print.cvc		diff \| blob \| history
test/regress/regress0/cvc3-bug15.cvc		diff \| blob \| history
test/regress/regress0/cvc3.userdoc.01.cvc		diff \| blob \| history
test/regress/regress0/cvc3.userdoc.02.cvc		diff \| blob \| history
test/regress/regress0/cvc3.userdoc.03.cvc		diff \| blob \| history
test/regress/regress0/cvc3.userdoc.04.cvc		diff \| blob \| history
test/regress/regress0/cvc3.userdoc.05.cvc		diff \| blob \| history
test/regress/regress0/cvc3.userdoc.06.cvc		diff \| blob \| history
test/regress/regress0/datatypes/bug286.cvc		diff \| blob \| history
test/regress/regress0/datatypes/datatype-dump.cvc		diff \| blob \| history
test/regress/regress0/datatypes/datatype.cvc		diff \| blob \| history
test/regress/regress0/datatypes/datatype0.cvc		diff \| blob \| history
test/regress/regress0/datatypes/datatype1.cvc		diff \| blob \| history
test/regress/regress0/datatypes/datatype13.cvc		diff \| blob \| history
test/regress/regress0/datatypes/datatype2.cvc		diff \| blob \| history
test/regress/regress0/datatypes/datatype3.cvc		diff \| blob \| history
test/regress/regress0/datatypes/datatype4.cvc		diff \| blob \| history
test/regress/regress0/datatypes/empty_tuprec.cvc		diff \| blob \| history
test/regress/regress0/datatypes/mutually-recursive.cvc		diff \| blob \| history
test/regress/regress0/datatypes/rec1.cvc		diff \| blob \| history
test/regress/regress0/datatypes/rec2.cvc		diff \| blob \| history
test/regress/regress0/datatypes/rec4.cvc		diff \| blob \| history
test/regress/regress0/datatypes/rewriter.cvc		diff \| blob \| history
test/regress/regress0/datatypes/tuple-record-bug.cvc		diff \| blob \| history
test/regress/regress0/datatypes/tuple.cvc		diff \| blob \| history
test/regress/regress0/datatypes/typed_v10l30054.cvc		diff \| blob \| history
test/regress/regress0/datatypes/typed_v1l80005.cvc		diff \| blob \| history
test/regress/regress0/datatypes/typed_v2l30079.cvc		diff \| blob \| history
test/regress/regress0/datatypes/typed_v3l20092.cvc		diff \| blob \| history
test/regress/regress0/datatypes/typed_v5l30069.cvc		diff \| blob \| history
test/regress/regress0/datatypes/v10l40099.cvc		diff \| blob \| history
test/regress/regress0/datatypes/v2l40025.cvc		diff \| blob \| history
test/regress/regress0/datatypes/v3l60006.cvc		diff \| blob \| history
test/regress/regress0/datatypes/v5l30058.cvc		diff \| blob \| history
test/regress/regress0/datatypes/wrong-sel-simp.cvc		diff \| blob \| history
test/regress/regress0/fmf/bug-041417-set-options.cvc		diff \| blob \| history
test/regress/regress0/let.cvc		diff \| blob \| history
test/regress/regress0/logops.01.cvc		diff \| blob \| history
test/regress/regress0/logops.02.cvc		diff \| blob \| history
test/regress/regress0/logops.03.cvc		diff \| blob \| history
test/regress/regress0/logops.04.cvc		diff \| blob \| history
test/regress/regress0/logops.05.cvc		diff \| blob \| history
test/regress/regress0/precedence/and-not.cvc		diff \| blob \| history
test/regress/regress0/precedence/and-xor.cvc		diff \| blob \| history
test/regress/regress0/precedence/bool-cmp.cvc		diff \| blob \| history
test/regress/regress0/precedence/cmp-plus.cvc		diff \| blob \| history
test/regress/regress0/precedence/eq-fun.cvc		diff \| blob \| history
test/regress/regress0/precedence/iff-assoc.cvc		diff \| blob \| history
test/regress/regress0/precedence/iff-implies.cvc		diff \| blob \| history
test/regress/regress0/precedence/implies-assoc.cvc		diff \| blob \| history
test/regress/regress0/precedence/implies-iff.cvc		diff \| blob \| history
test/regress/regress0/precedence/implies-or.cvc		diff \| blob \| history
test/regress/regress0/precedence/not-and.cvc		diff \| blob \| history
test/regress/regress0/precedence/not-eq.cvc		diff \| blob \| history
test/regress/regress0/precedence/or-implies.cvc		diff \| blob \| history
test/regress/regress0/precedence/or-xor.cvc		diff \| blob \| history
test/regress/regress0/precedence/plus-mult.cvc		diff \| blob \| history
test/regress/regress0/precedence/xor-and.cvc		diff \| blob \| history
test/regress/regress0/precedence/xor-assoc.cvc		diff \| blob \| history
test/regress/regress0/precedence/xor-or.cvc		diff \| blob \| history
test/regress/regress0/preprocess/preprocess_00.cvc		diff \| blob \| history
test/regress/regress0/preprocess/preprocess_02.cvc		diff \| blob \| history
test/regress/regress0/preprocess/preprocess_06.cvc		diff \| blob \| history
test/regress/regress0/preprocess/preprocess_13.cvc		diff \| blob \| history
test/regress/regress0/printer/tuples_and_records.cvc		diff \| blob \| history
test/regress/regress0/push-pop/bug233.cvc		diff \| blob \| history
test/regress/regress0/push-pop/incremental-subst-bug.cvc		diff \| blob \| history
test/regress/regress0/quantifiers/cegqi-nl-simp.cvc		diff \| blob \| history
test/regress/regress0/sets/cvc-sample.cvc		diff \| blob \| history
test/regress/regress0/simple.cvc		diff \| blob \| history
test/regress/regress0/smallcnf.cvc		diff \| blob \| history
test/regress/regress0/smtlib/set-info-status.smt2		diff \| blob \| history
test/regress/regress0/test11.cvc		diff \| blob \| history
test/regress/regress0/test9.cvc		diff \| blob \| history
test/regress/regress0/uf/simple.01.cvc		diff \| blob \| history
test/regress/regress0/uf/simple.02.cvc		diff \| blob \| history
test/regress/regress0/uf/simple.03.cvc		diff \| blob \| history
test/regress/regress0/uf/simple.04.cvc		diff \| blob \| history
test/regress/regress0/uf20-03.cvc		diff \| blob \| history
test/regress/regress0/wiki.01.cvc		diff \| blob \| history
test/regress/regress0/wiki.02.cvc		diff \| blob \| history
test/regress/regress0/wiki.03.cvc		diff \| blob \| history
test/regress/regress0/wiki.04.cvc		diff \| blob \| history
test/regress/regress0/wiki.05.cvc		diff \| blob \| history
test/regress/regress0/wiki.06.cvc		diff \| blob \| history
test/regress/regress0/wiki.07.cvc		diff \| blob \| history
test/regress/regress0/wiki.08.cvc		diff \| blob \| history
test/regress/regress0/wiki.09.cvc		diff \| blob \| history
test/regress/regress0/wiki.10.cvc		diff \| blob \| history
test/regress/regress0/wiki.11.cvc		diff \| blob \| history
test/regress/regress0/wiki.12.cvc		diff \| blob \| history
test/regress/regress0/wiki.13.cvc		diff \| blob \| history
test/regress/regress0/wiki.14.cvc		diff \| blob \| history
test/regress/regress0/wiki.15.cvc		diff \| blob \| history
test/regress/regress0/wiki.16.cvc		diff \| blob \| history
test/regress/regress0/wiki.17.cvc		diff \| blob \| history
test/regress/regress0/wiki.18.cvc		diff \| blob \| history
test/regress/regress0/wiki.19.cvc		diff \| blob \| history
test/regress/regress0/wiki.20.cvc		diff \| blob \| history
test/regress/regress0/wiki.21.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-001.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-002.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-003.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-004.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-005.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-006.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-007.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-008.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-009.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-010.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-011.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-012.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-013.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-016.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-017.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-018.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-019.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-020.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-022.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-024.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-026.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-027.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-028.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-029.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-030.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-031.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-032.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-033.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-034.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-035.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-036.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-037.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-038.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-039.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-040.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-041.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-043.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-044.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-045.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-046.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-047.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-048.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-049.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-050.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-051.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-052.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-053.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-054.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-055.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-056.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-057.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-058.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-059.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-060.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-061.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-062.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-063.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-064.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-065.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-066.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-067.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-068.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-069.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-070.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-071.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-072.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-073.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-074.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-075.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-076.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-077.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-078.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-080.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-081.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-082.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-083.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-084.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-085.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-086.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-087.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-088.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-089.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-090.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-091.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-092.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-093.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-094.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-095.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-096.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-097.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-099.cvc		diff \| blob \| history
test/regress/regress1/arith/arith-int-100.cvc		diff \| blob \| history
test/regress/regress1/boolean.cvc		diff \| blob \| history
test/regress/regress1/fmf/ko-bound-set.cvc		diff \| blob \| history
test/regress/regress1/hole6.cvc		diff \| blob \| history
test/regress/regress1/quantifiers/set-choice-koikonomou.cvc		diff \| blob \| history
test/regress/regress1/test12.cvc		diff \| blob \| history
test/regress/regress2/arith/arith-int-098.cvc		diff \| blob \| history
test/regress/regress2/hole7.cvc		diff \| blob \| history
test/regress/regress2/hole8.cvc		diff \| blob \| history
test/regress/regress2/typed_v1l50016-simp.cvc		diff \| blob \| history
test/regress/regress3/hole9.cvc		diff \| blob \| history
test/regress/regress4/hole10.cvc		diff \| blob \| history
test/system/boilerplate.cpp		diff \| blob \| history
test/system/statistics.cpp		diff \| blob \| history
test/system/two_smt_engines.cpp		diff \| blob \| history
test/unit/api/result_black.h		diff \| blob \| history
test/unit/api/solver_black.h		diff \| blob \| history

RSS Atom