| ||||
| ||||
![]() Title:From MBQI to Enumerative Instantiation and Back Conference:SMT 2025 Tags:enumerative, ground part, ground term, ground terms, MBQI, preferred terms, quantified variable, quantifier instantiation, SMT, theories with quantifiers and uninterpreted function Abstract: This work investigates the relation between model-based quantifier instantiation (MBQI) and enumerative instantiation (EI) in Satisfiability Modulo Theories (SMT). MBQI operates at the semantic level and guarantees to find an counter-example to a given a non-model. However, it may lead to weak instantiations. In contrast, EI strives for completeness by systematically enumerating terms at the syntactic level. However, such terms may not be counter-examples. Here we investigate the relation between the two techniques and report on our initial experiments of the proposed algorithm that combines the two. From MBQI to Enumerative Instantiation and Back ![]() From MBQI to Enumerative Instantiation and Back | ||||
Copyright © 2002 – 2025 EasyChair |