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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Tue, 22 Mar 2022 01:27:20 +0000 (20:27 -0500)
committer	GitHub <noreply@github.com>
	Tue, 22 Mar 2022 01:27:20 +0000 (01:27 +0000)
commit	c914f3eca82aaf51dd9a208574dab6aa3b000201
tree	376eb7864675c428cae9c36383d6a3902d7e0017	tree
parent	4a58ed7daf86dd0b9cd1dabc9d83458da1fb23ae	commit \| diff

Refactor result class (#8313)

This significantly refactors the internal result class. Entailments and "which" field are deleted, "Sat" is renamed to "Status". Moreover "TYPE_NONE" is made into a status.

Simplifies the usage of this class throughout the code.

It also changes the API Result method isSatUnknown to isUnknown.

58 files changed:

src/api/cpp/cvc5.cpp		diff \| blob \| history
src/api/cpp/cvc5.h		diff \| blob \| history
src/api/java/io/github/cvc5/api/Result.java		diff \| blob \| history
src/api/java/jni/result.cpp		diff \| blob \| history
src/api/python/cvc5.pxd		diff \| blob \| history
src/api/python/cvc5.pxi		diff \| blob \| history
src/main/command_executor.cpp		diff \| blob \| history
src/omt/bitvector_optimizer.cpp		diff \| blob \| history
src/omt/integer_optimizer.cpp		diff \| blob \| history
src/prop/prop_engine.cpp		diff \| blob \| history
src/smt/abduction_solver.cpp		diff \| blob \| history
src/smt/assertions.cpp		diff \| blob \| history
src/smt/command.cpp		diff \| blob \| history
src/smt/interpolation_solver.cpp		diff \| blob \| history
src/smt/optimization_solver.cpp		diff \| blob \| history
src/smt/optimization_solver.h		diff \| blob \| history
src/smt/quant_elim_solver.cpp		diff \| blob \| history
src/smt/smt_mode.cpp		diff \| blob \| history
src/smt/smt_solver.cpp		diff \| blob \| history
src/smt/solver_engine.cpp		diff \| blob \| history
src/smt/solver_engine.h		diff \| blob \| history
src/smt/solver_engine_state.cpp		diff \| blob \| history
src/smt/sygus_solver.cpp		diff \| blob \| history
src/theory/arith/attempt_solution_simplex.cpp		diff \| blob \| history
src/theory/arith/attempt_solution_simplex.h		diff \| blob \| history
src/theory/arith/dual_simplex.cpp		diff \| blob \| history
src/theory/arith/dual_simplex.h		diff \| blob \| history
src/theory/arith/fc_simplex.cpp		diff \| blob \| history
src/theory/arith/fc_simplex.h		diff \| blob \| history
src/theory/arith/nl/nonlinear_extension.cpp		diff \| blob \| history
src/theory/arith/nl/nonlinear_extension.h		diff \| blob \| history
src/theory/arith/simplex.h		diff \| blob \| history
src/theory/arith/soi_simplex.cpp		diff \| blob \| history
src/theory/arith/soi_simplex.h		diff \| blob \| history
src/theory/arith/theory_arith_private.cpp		diff \| blob \| history
src/theory/arith/theory_arith_private.h		diff \| blob \| history
src/theory/quantifiers/candidate_rewrite_database.cpp		diff \| blob \| history
src/theory/quantifiers/query_generator.cpp		diff \| blob \| history
src/theory/quantifiers/query_generator_sample_sat.cpp		diff \| blob \| history
src/theory/quantifiers/query_generator_unsat.cpp		diff \| blob \| history
src/theory/quantifiers/solution_filter.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/ce_guided_single_inv.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/cegis_core_connective.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_interpol.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_repair_const.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/synth_conjecture.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/synth_verify.cpp		diff \| blob \| history
src/theory/smt_engine_subsolver.cpp		diff \| blob \| history
src/util/result.cpp		diff \| blob \| history
src/util/result.h		diff \| blob \| history
test/unit/api/cpp/result_black.cpp		diff \| blob \| history
test/unit/api/java/ResultTest.java		diff \| blob \| history
test/unit/api/python/test_result.py		diff \| blob \| history
test/unit/theory/theory_bv_opt_white.cpp		diff \| blob \| history
test/unit/theory/theory_bv_white.cpp		diff \| blob \| history
test/unit/theory/theory_int_opt_white.cpp		diff \| blob \| history
test/unit/theory/theory_opt_multigoal_white.cpp		diff \| blob \| history
test/unit/theory/theory_quantifiers_bv_inverter_white.cpp		diff \| blob \| history

RSS Atom