projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 6cf3a69) | patch
Eliminate currentSmtEngine for subsolver calls (#7068)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 26 Aug 2021 16:55:59 +0000 (11:55 -0500)
committerGitHub <noreply@github.com>
Thu, 26 Aug 2021 16:55:59 +0000 (16:55 +0000)
commit21fa888738ea77e4436ef164c184e61683a55fb5
treeaf76cfe9dbbb082ee8e2ed73afa974daf2fb0f07tree
parent6cf3a69a9afd68922d67941c6fd2b877df45ecb9commit | diff
Eliminate currentSmtEngine for subsolver calls (#7068)

This eliminates another occurrence of smt::currentSmtEngine by making it required to pass options + logic for all subsolver calls.
43 files changed:
src/preprocessing/passes/sygus_inference.cpp diff | blob | history
src/preprocessing/preprocessing_pass_context.cpp diff | blob | history
src/preprocessing/preprocessing_pass_context.h diff | blob | history
src/smt/abduction_solver.cpp diff | blob | history
src/smt/abduction_solver.h diff | blob | history
src/smt/env.cpp diff | blob | history
src/smt/env.h diff | blob | history
src/smt/interpolation_solver.cpp diff | blob | history
src/smt/interpolation_solver.h 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/quant_elim_solver.h diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
src/smt/smt_engine.h diff | blob | history
src/smt/sygus_solver.cpp diff | blob | history
src/smt/sygus_solver.h diff | blob | history
src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp diff | blob | history
src/theory/quantifiers/cegqi/nested_qe.cpp diff | blob | history
src/theory/quantifiers/cegqi/nested_qe.h diff | blob | history
src/theory/quantifiers/expr_miner.cpp diff | blob | history
src/theory/quantifiers/sygus/ce_guided_single_inv.cpp diff | blob | history
src/theory/quantifiers/sygus/ce_guided_single_inv.h diff | blob | history
src/theory/quantifiers/sygus/cegis.cpp diff | blob | history
src/theory/quantifiers/sygus/cegis.h diff | blob | history
src/theory/quantifiers/sygus/cegis_core_connective.cpp diff | blob | history
src/theory/quantifiers/sygus/cegis_core_connective.h diff | blob | history
src/theory/quantifiers/sygus/cegis_unif.cpp diff | blob | history
src/theory/quantifiers/sygus/sygus_interpol.cpp diff | blob | history
src/theory/quantifiers/sygus/sygus_interpol.h diff | blob | history
src/theory/quantifiers/sygus/sygus_module.cpp diff | blob | history
src/theory/quantifiers/sygus/sygus_module.h diff | blob | history
src/theory/quantifiers/sygus/sygus_pbe.cpp diff | blob | history
src/theory/quantifiers/sygus/sygus_pbe.h diff | blob | history
src/theory/quantifiers/sygus/sygus_qe_preproc.cpp diff | blob | history
src/theory/quantifiers/sygus/sygus_qe_preproc.h 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_engine.cpp diff | blob | history
src/theory/quantifiers/sygus/synth_verify.cpp diff | blob | history
src/theory/quantifiers/sygus/synth_verify.h diff | blob | history
src/theory/smt_engine_subsolver.cpp diff | blob | history
src/theory/smt_engine_subsolver.h diff | blob | history