From daf2eca9a4bb32680cbf35945bb09cfd13be76a7 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Wed, 20 Jul 2016 11:52:37 -0500 Subject: [PATCH] Print only instantiations that are in the unsat core when --proof is enabled. Add option to minimize sygus solutions based on unsat core (disabled by default). --- src/options/quantifiers_options | 2 ++ src/theory/quantifiers/ce_guided_single_inv.cpp | 5 +---- src/theory/quantifiers_engine.cpp | 7 ++++--- 3 files changed, 7 insertions(+), 7 deletions(-) diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index 0a94ad890..37178510d 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -242,6 +242,8 @@ option cegqiSingleInvPartial --cegqi-si-partial bool :default false combined techniques for synthesis conjectures that are partially single invocation option cegqiSingleInvReconstruct --cegqi-si-reconstruct bool :default true reconstruct solutions for single invocation conjectures in original grammar +option cegqiSolMinCore --cegqi-si-sol-min-core bool :default false + minimize solutions for single invocation conjectures based on unsat core option cegqiSingleInvReconstructConst --cegqi-si-reconstruct-const bool :default true include constants when reconstruct solutions for single invocation conjectures in original grammar option cegqiSingleInvAbort --cegqi-si-abort bool :default false diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp index facd7bd2e..3f781774d 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv.cpp @@ -755,13 +755,10 @@ Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int& Trace("csi-sol") << "Sort solution return values " << sol_index << std::endl; bool useUnsatCore = false; std::vector< Node > active_lemmas; - /* TODO? //minimize based on unsat core, if possible - std::vector< Node > active_lemmas; - if( d_qe->getUnsatCoreLemmas( active_lemmas ) ){ + if( options::cegqiSolMinCore() && d_qe->getUnsatCoreLemmas( active_lemmas ) ){ useUnsatCore = true; } - */ Assert( d_lemmas_produced.size()==d_inst.size() ); std::vector< unsigned > indices; for( unsigned i=0; i& active_lemmas ) { - //TODO: only if unsat core available + //only if unsat core available bool isUnsatCoreAvailable = false; - //if( options::proof() ){ - //} + if( options::proof() ){ + isUnsatCoreAvailable = ProofManager::currentPM()->unsatCoreAvailable(); + } if( isUnsatCoreAvailable ){ Trace("inst-unsat-core") << "Get instantiations in unsat core..." << std::endl; ProofManager::currentPM()->getLemmasInUnsatCore(theory::THEORY_QUANTIFIERS, active_lemmas); -- 2.30.2