diff options
| -rw-r--r-- | src/options/quantifiers_options | 2 | ||||
| -rw-r--r-- | src/theory/quantifiers/ce_guided_single_inv.cpp | 5 | ||||
| -rw-r--r-- | 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<d_lemmas_produced.size(); i++ ){ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 59fa3592d..da8233fc1 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -1286,10 +1286,11 @@ void QuantifiersEngine::flushLemmas(){ } bool QuantifiersEngine::getUnsatCoreLemmas( std::vector< Node >& 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); |