From 4cff52d94318646415fe89dfe3b97750451eb7c1 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Tue, 26 Jul 2016 17:55:09 -0500 Subject: [PATCH] Add option to minimize sygus solutions based on using weakest implicants of instantiations in unsat cores. --- src/options/quantifiers_options | 2 ++ .../quantifiers/ce_guided_single_inv.cpp | 24 +++++++++++++++---- src/theory/quantifiers/ce_guided_single_inv.h | 2 +- src/theory/quantifiers_engine.cpp | 15 ++++++++++++ src/theory/quantifiers_engine.h | 1 + 5 files changed, 38 insertions(+), 6 deletions(-) diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index 37178510d..953150e42 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -244,6 +244,8 @@ 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 cegqiSolMinInst --cegqi-si-sol-min-inst bool :default true + minimize individual instantiations 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 3f781774d..981abea94 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv.cpp @@ -658,7 +658,7 @@ bool CegConjectureSingleInv::check( std::vector< Node >& lems ) { } } -Node CegConjectureSingleInv::constructSolution( std::vector< unsigned >& indices, unsigned i, unsigned index ) { +Node CegConjectureSingleInv::constructSolution( std::vector< unsigned >& indices, unsigned i, unsigned index, std::map< Node, Node >& weak_imp ) { Assert( index& indices return d_inst[uindex][i]; }else{ Node cond = d_lemmas_produced[uindex]; + //weaken based on unsat core + std::map< Node, Node >::iterator itw = weak_imp.find( cond ); + if( itw!=weak_imp.end() ){ + cond = itw->second; + } cond = TermDb::simpleNegate( cond ); Node ite1 = d_inst[uindex][i]; - Node ite2 = constructSolution( indices, i, index+1 ); + Node ite2 = constructSolution( indices, i, index+1, weak_imp ); return NodeManager::currentNM()->mkNode( ITE, cond, ite1, ite2 ); } } @@ -756,8 +761,17 @@ Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int& bool useUnsatCore = false; std::vector< Node > active_lemmas; //minimize based on unsat core, if possible - if( options::cegqiSolMinCore() && d_qe->getUnsatCoreLemmas( active_lemmas ) ){ - useUnsatCore = true; + std::map< Node, Node > weak_imp; + if( options::cegqiSolMinCore() ){ + if( options::cegqiSolMinInst() ){ + if( d_qe->getUnsatCoreLemmas( active_lemmas, weak_imp ) ){ + useUnsatCore = true; + } + }else{ + if( d_qe->getUnsatCoreLemmas( active_lemmas ) ){ + useUnsatCore = true; + } + } } Assert( d_lemmas_produced.size()==d_inst.size() ); std::vector< unsigned > indices; @@ -780,7 +794,7 @@ Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int& ssii.d_i = sol_index; std::sort( indices.begin(), indices.end(), ssii ); Trace("csi-sol") << "Construct solution" << std::endl; - s = constructSolution( indices, sol_index, 0 ); + s = constructSolution( indices, sol_index, 0, weak_imp ); Assert( vars.size()==d_sol->d_varList.size() ); s = s.substitute( vars.begin(), vars.end(), d_sol->d_varList.begin(), d_sol->d_varList.end() ); } diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h index 4d2f9a0e5..feadeca39 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.h +++ b/src/theory/quantifiers/ce_guided_single_inv.h @@ -74,7 +74,7 @@ private: std::map< Node, std::vector< Node > >& teq, Node n, std::vector< Node >& conj ); //constructing solution - Node constructSolution( std::vector< unsigned >& indices, unsigned i, unsigned index ); + Node constructSolution( std::vector< unsigned >& indices, unsigned i, unsigned index, std::map< Node, Node >& weak_imp ); Node postProcessSolution( Node n ); private: //list of skolems for each argument of programs 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() ){ diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 1ba0b6572..08ca0564b 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -368,6 +368,7 @@ public: void getInstantiations( std::map< Node, std::vector< Node > >& insts ); /** get unsat core lemmas */ bool getUnsatCoreLemmas( std::vector< Node >& active_lemmas ); + bool getUnsatCoreLemmas( std::vector< Node >& active_lemmas, std::map< Node, Node >& weak_imp ); /** get inst for lemmas */ void getExplanationForInstLemmas( std::vector< Node >& lems, std::map< Node, Node >& quant, std::map< Node, std::vector< Node > >& tvec ); /** statistics class */ -- 2.30.2