From c7f50a009cad7a0c1a2f1a5290e1d7bd03edf0e7 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 11 Mar 2020 11:27:40 -0500 Subject: [PATCH] Remove partial instantiation for local theory extensions (#4020) Fixes #4019. This feature was never fully implemented. --- src/CMakeLists.txt | 2 - src/options/quantifiers_options.toml | 9 - src/theory/quantifiers/local_theory_ext.cpp | 270 -------------------- src/theory/quantifiers/local_theory_ext.h | 93 ------- src/theory/quantifiers_engine.cpp | 9 - 5 files changed, 383 deletions(-) delete mode 100644 src/theory/quantifiers/local_theory_ext.cpp delete mode 100644 src/theory/quantifiers/local_theory_ext.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 5b07a7ca6..0908b5b68 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -517,8 +517,6 @@ libcvc4_add_sources( theory/quantifiers/instantiate.h theory/quantifiers/lazy_trie.cpp theory/quantifiers/lazy_trie.h - theory/quantifiers/local_theory_ext.cpp - theory/quantifiers/local_theory_ext.h theory/quantifiers/quant_conflict_find.cpp theory/quantifiers/quant_conflict_find.h theory/quantifiers/quant_epr.cpp diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 926eacaae..e104101ef 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -1934,15 +1934,6 @@ header = "options/quantifiers_options.h" read_only = true help = "do instantiation based on local theory extensions" -[[option]] - name = "ltePartialInst" - category = "regular" - long = "lte-partial-inst" - type = "bool" - default = "false" - read_only = true - help = "partially instantiate local theory quantifiers" - [[option]] name = "lteRestrictInstClosure" category = "regular" diff --git a/src/theory/quantifiers/local_theory_ext.cpp b/src/theory/quantifiers/local_theory_ext.cpp deleted file mode 100644 index a3de5ced9..000000000 --- a/src/theory/quantifiers/local_theory_ext.cpp +++ /dev/null @@ -1,270 +0,0 @@ -/********************* */ -/*! \file local_theory_ext.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters, Paul Meng - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Implementation of local theory ext utilities - **/ - -#include "theory/quantifiers/local_theory_ext.h" -#include "theory/quantifiers/term_database.h" -#include "theory/quantifiers/term_util.h" -#include "theory/quantifiers_engine.h" -#include "theory/quantifiers/first_order_model.h" - -using namespace std; -using namespace CVC4; -using namespace CVC4::kind; -using namespace CVC4::context; -using namespace CVC4::theory; -using namespace CVC4::theory::quantifiers; - - -LtePartialInst::LtePartialInst( QuantifiersEngine * qe, context::Context* c ) : -QuantifiersModule( qe ), d_wasInvoked( false ), d_needsCheck( false ){ - -} - -/** add quantifier */ -void LtePartialInst::checkOwnership(Node q) -{ - if( !q.getAttribute(LtePartialInstAttribute()) ){ - if( d_do_inst.find( q )!=d_do_inst.end() ){ - if( d_do_inst[q] ){ - d_lte_asserts.push_back( q ); - d_quantEngine->setOwner( q, this ); - } - }else{ - d_vars[q].clear(); - d_pat_var_order[q].clear(); - //check if this quantified formula is eligible for partial instantiation - std::map< Node, bool > vars; - for( unsigned i=0; i var_order; - bool doInst = true; - for( unsigned i=0; isetOwner( q, this ); - } - } - } -} - -bool LtePartialInst::addVariableToPatternList( Node v, std::vector< int >& pat_var_order, std::map< Node, int >& var_order ) { - std::map< Node, int >::iterator it = var_order.find( v ); - if( it==var_order.end() ){ - return false; - }else if( std::find( pat_var_order.begin(), pat_var_order.end(), it->second )!=pat_var_order.end() ){ - return false; - }else{ - pat_var_order.push_back( it->second ); - return true; - } -} - -void LtePartialInst::getEligibleInstVars( Node n, std::map< Node, bool >& vars ) { - if( n.getKind()==APPLY_UF && !n.getType().isBoolean() ){ - for( unsigned i=0; i=Theory::EFFORT_FULL && d_needsCheck; -} -/* Call during quantifier engine's check */ -void LtePartialInst::check(Theory::Effort e, QEffort quant_e) -{ - //flush lemmas ASAP (they are a reduction) - if (quant_e == QEFFORT_CONFLICT && d_needsCheck) - { - std::vector< Node > lemmas; - getInstantiations( lemmas ); - //add lemmas to quantifiers engine - for( unsigned i=0; iaddLemma( lemmas[i], false ); - } - d_needsCheck = false; - } -} - - -void LtePartialInst::reset() { - d_reps.clear(); - eq::EqualityEngine* ee = d_quantEngine->getActiveEqualityEngine(); - eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee ); - while( !eqcs_i.isFinished() ){ - TNode r = (*eqcs_i); - TypeNode tn = r.getType(); - d_reps[tn].push_back( r ); - ++eqcs_i; - } -} - - -/** get instantiations */ -void LtePartialInst::getInstantiations( std::vector< Node >& lemmas ) { - Trace("lte-partial-inst") << "LTE : get instantiations, # quant = " << d_lte_asserts.size() << std::endl; - reset(); - for( unsigned i=0; i bvs; - for( unsigned j=0; jmkNode( BOUND_VAR_LIST, bvs ); - } - std::vector< Node > conj; - std::vector< Node > terms; - std::vector< TypeNode > types; - for( unsigned j=0; jmkNode( OR, q.negate(), conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( AND, conj ) ) ); - d_wasInvoked = true; - } - } -} - -void LtePartialInst::getPartialInstantiations(std::vector& conj, - Node q, - Node bvl, - std::vector& vars, - std::vector& terms, - std::vector& types, - TNodeTrie* curr, - unsigned pindex, - unsigned paindex, - unsigned iindex) -{ - if( iindex==vars.size() ){ - Node body = q[1].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ); - if( bvl.isNull() ){ - conj.push_back( body ); - Trace("lte-partial-inst") << " - ground conjunct : " << body << std::endl; - }else{ - Node nq; - if( q.getNumChildren()==3 ){ - Node ipl = q[2].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ); - nq = NodeManager::currentNM()->mkNode( FORALL, bvl, body, ipl ); - }else{ - nq = NodeManager::currentNM()->mkNode( FORALL, bvl, body ); - } - Trace("lte-partial-inst") << " - quantified conjunct : " << nq << std::endl; - LtePartialInstAttribute ltpia; - nq.setAttribute(ltpia,true); - conj.push_back( nq ); - } - }else{ - Assert(pindex < q[2][0].getNumChildren()); - Node pat = q[2][0][pindex]; - Assert(pat.getNumChildren() == 0 || paindex <= pat.getNumChildren()); - if( pat.getKind()==APPLY_UF ){ - Assert(paindex <= pat.getNumChildren()); - if( paindex==pat.getNumChildren() ){ - getPartialInstantiations( conj, q, bvl, vars, terms, types, NULL, pindex+1, 0, iindex ); - }else{ - if( !curr ){ - Assert(paindex == 0); - //start traversing term index for the operator - curr = d_quantEngine->getTermDatabase()->getTermArgTrie( pat.getOperator() ); - } - for (std::pair& t : curr->d_data) - { - terms[d_pat_var_order[q][iindex]] = t.first; - getPartialInstantiations(conj, - q, - bvl, - vars, - terms, - types, - &t.second, - pindex, - paindex + 1, - iindex + 1); - } - } - }else{ - std::map< TypeNode, std::vector< Node > >::iterator it = d_reps.find( types[iindex] ); - if( it!=d_reps.end() ){ - Trace("lte-partial-inst-debug") << it->second.size() << " reps of type " << types[iindex] << std::endl; - for( unsigned i=0; isecond.size(); i++ ){ - terms[d_pat_var_order[q][iindex]] = it->second[i]; - getPartialInstantiations( conj, q, bvl, vars, terms, types, NULL, pindex+1, 0, iindex+1 ); - } - }else{ - Trace("lte-partial-inst-debug") << "No reps found of type " << types[iindex] << std::endl; - } - } - } -} diff --git a/src/theory/quantifiers/local_theory_ext.h b/src/theory/quantifiers/local_theory_ext.h deleted file mode 100644 index d39ea3cfe..000000000 --- a/src/theory/quantifiers/local_theory_ext.h +++ /dev/null @@ -1,93 +0,0 @@ -/********************* */ -/*! \file local_theory_ext.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Mathias Preiner - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief local theory extensions util - **/ - -#include "cvc4_private.h" - -#ifndef CVC4__THEORY__LOCAL_THEORY_EXT_H -#define CVC4__THEORY__LOCAL_THEORY_EXT_H - -#include "context/cdo.h" -#include "expr/attribute.h" -#include "expr/node_trie.h" -#include "theory/quantifiers/quant_util.h" - -namespace CVC4 { -namespace theory { - -/** Attribute true for quantifiers that do not need to be partially instantiated - */ -struct LtePartialInstAttributeId -{ -}; -typedef expr::Attribute - LtePartialInstAttribute; - -namespace quantifiers { - -class LtePartialInst : public QuantifiersModule { -private: - // was this module invoked - bool d_wasInvoked; - // needs check - bool d_needsCheck; - //representatives per type - std::map< TypeNode, std::vector< Node > > d_reps; - // should we instantiate quantifier - std::map< Node, bool > d_do_inst; - // have we instantiated quantifier - std::map< Node, bool > d_inst; - std::map< Node, std::vector< Node > > d_vars; - std::map< Node, std::vector< int > > d_pat_var_order; - /** list of relevant quantifiers asserted in the current context */ - std::vector< Node > d_lte_asserts; - /** reset */ - void reset(); - /** get instantiations */ - void getInstantiations( std::vector< Node >& lemmas ); - void getPartialInstantiations(std::vector& conj, - Node q, - Node bvl, - std::vector& vars, - std::vector& inst, - std::vector& types, - TNodeTrie* curr, - unsigned pindex, - unsigned paindex, - unsigned iindex); - /** get eligible inst variables */ - void getEligibleInstVars( Node n, std::map< Node, bool >& vars ); - - bool addVariableToPatternList( Node v, std::vector< int >& pat_var_order, std::map< Node, int >& var_order ); -public: - LtePartialInst( QuantifiersEngine * qe, context::Context* c ); - /** determine whether this quantified formula will be reduced */ - void checkOwnership(Node q) override; - /** was invoked */ - bool wasInvoked() { return d_wasInvoked; } - - /* whether this module needs to check this round */ - bool needsCheck(Theory::Effort e) override; - /* Call during quantifier engine's check */ - void check(Theory::Effort e, QEffort quant_e) override; - /* check complete */ - bool checkComplete() override { return !d_wasInvoked; } - /** Identify this module (for debugging, dynamic configuration, etc..) */ - std::string identify() const override { return "LtePartialInst"; } -}; - -} -} -} - -#endif diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index ed4a79808..4339ee75f 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -25,7 +25,6 @@ #include "theory/quantifiers/fmf/full_model_check.h" #include "theory/quantifiers/fmf/model_engine.h" #include "theory/quantifiers/inst_strategy_enumerative.h" -#include "theory/quantifiers/local_theory_ext.h" #include "theory/quantifiers/quant_conflict_find.h" #include "theory/quantifiers/quant_split.h" #include "theory/quantifiers/quantifiers_rewriter.h" @@ -52,7 +51,6 @@ class QuantifiersEnginePrivate d_qcf(nullptr), d_sg_gen(nullptr), d_synth_e(nullptr), - d_lte_part_inst(nullptr), d_fs(nullptr), d_i_cbqi(nullptr), d_qsplit(nullptr), @@ -79,8 +77,6 @@ class QuantifiersEnginePrivate std::unique_ptr d_sg_gen; /** ceg instantiation */ std::unique_ptr d_synth_e; - /** lte partial instantiation */ - std::unique_ptr d_lte_part_inst; /** full saturation */ std::unique_ptr d_fs; /** counterexample-based quantifier instantiation */ @@ -142,11 +138,6 @@ class QuantifiersEnginePrivate // finite model finder has special ways of building the model needsBuilder = true; } - if (options::ltePartialInst()) - { - d_lte_part_inst.reset(new quantifiers::LtePartialInst(qe, c)); - modules.push_back(d_lte_part_inst.get()); - } if (options::quantDynamicSplit() != options::QuantDSplitMode::NONE) { d_qsplit.reset(new quantifiers::QuantDSplit(qe, c)); -- 2.30.2