projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 255d19b) | patch
Refactor mkRep option for instantiation (#8657)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 26 Apr 2022 19:56:40 +0000 (14:56 -0500)
committerGitHub <noreply@github.com>
Tue, 26 Apr 2022 19:56:40 +0000 (19:56 +0000)
commit28869764c41725a0c98df4f1b8de5bfd618551c3
treebabbe399f0d9c8c78dfec34a23fd807de4d6f613tree
parent255d19b17351335bfec73ecc10d5c40770a3f17bcommit | diff
Refactor mkRep option for instantiation (#8657)

This removes mkRep as an option for addInstantiation.

It adds a new interface for making term vectors representative, which is required for FMF instantiation.
src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp diff | blob | history
src/theory/quantifiers/fmf/full_model_check.cpp diff | blob | history
src/theory/quantifiers/fmf/model_engine.cpp diff | blob | history
src/theory/quantifiers/instantiate.cpp diff | blob | history
src/theory/quantifiers/instantiate.h diff | blob | history