diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-07-20 11:52:37 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-07-20 11:52:37 -0500 |
commit | daf2eca9a4bb32680cbf35945bb09cfd13be76a7 (patch) | |
tree | fd387c71b6d1bd03e79e4e3403041c12a906a98a /src/theory | |
parent | ae7434f94a1bc66ee12474414985249a71881b6c (diff) |
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).
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/quantifiers/ce_guided_single_inv.cpp | 5 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 7 |
2 files changed, 5 insertions, 7 deletions
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); |