From 4cff52d94318646415fe89dfe3b97750451eb7c1 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Tue, 26 Jul 2016 17:55:09 -0500 Subject: Add option to minimize sygus solutions based on using weakest implicants of instantiations in unsat cores. --- src/theory/quantifiers_engine.cpp | 15 +++++++++++++++ 1 file changed, 15 insertions(+) (limited to 'src/theory/quantifiers_engine.cpp') diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 2975d2e70..75d177fdc 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -1307,6 +1307,21 @@ bool QuantifiersEngine::getUnsatCoreLemmas( std::vector< Node >& active_lemmas ) } } +bool QuantifiersEngine::getUnsatCoreLemmas( std::vector< Node >& active_lemmas, std::map< Node, Node >& weak_imp ) { + if( getUnsatCoreLemmas( active_lemmas ) ){ + for (unsigned i = 0; i < active_lemmas.size(); ++i) { + Node n = ProofManager::currentPM()->getWeakestImplicantInUnsatCore(active_lemmas[i]); + if( n!=active_lemmas[i] ){ + Trace("inst-unsat-core") << " weaken : " << active_lemmas[i] << " -> " << n << std::endl; + } + weak_imp[active_lemmas[i]] = n; + } + return true; + }else{ + return false; + } +} + void QuantifiersEngine::getExplanationForInstLemmas( std::vector< Node >& lems, std::map< Node, Node >& quant, std::map< Node, std::vector< Node > >& tvec ) { if( d_trackInstLemmas ){ if( options::incrementalSolving() ){ -- cgit v1.2.3