diff options
Diffstat (limited to 'src/theory')
27 files changed, 491 insertions, 1832 deletions
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 65df3a642..283c70ada 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -41,24 +41,26 @@ namespace CVC4 { namespace theory { namespace datatypes { -TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out, - Valuation valuation, const LogicInfo& logicInfo) +TheoryDatatypes::TheoryDatatypes(Context* c, + UserContext* u, + OutputChannel& out, + Valuation valuation, + const LogicInfo& logicInfo) : Theory(THEORY_DATATYPES, c, u, out, valuation, logicInfo), - //d_cycle_check(c), - d_hasSeenCycle(c, false), d_infer(c), d_infer_exp(c), - d_term_sk( u ), - d_notify( *this ), + d_term_sk(u), + d_notify(*this), d_equalityEngine(d_notify, c, "theory::datatypes", true), - d_labels( c ), - d_selector_apps( c ), - //d_consEqc( c ), - d_conflict( c, false ), - d_collectTermsCache( c ), - d_functionTerms( c ), - d_singleton_eq( u ), - d_lemmas_produced_c( u ) + d_labels(c), + d_selector_apps(c), + d_conflict(c, false), + d_addedLemma(false), + d_addedFact(false), + d_collectTermsCache(c), + d_functionTerms(c), + d_singleton_eq(u), + d_lemmas_produced_c(u) { // The kinds we are treating as function application in congruence d_equalityEngine.addFunctionKind(kind::APPLY_CONSTRUCTOR); @@ -765,25 +767,6 @@ void TheoryDatatypes::conflict(TNode a, TNode b){ void TheoryDatatypes::eqNotifyNewClass(TNode t){ if( t.getKind()==APPLY_CONSTRUCTOR ){ getOrMakeEqcInfo( t, true ); - //look at all equivalence classes with constructor terms -/* - for( BoolMap::const_iterator it = d_consEqc.begin(); it != d_consEqc.end(); ++it ){ - if( (*it).second ){ - TNode r = (*it).first; - if( r.getType()==t.getType() ){ - EqcInfo * ei = getOrMakeEqcInfo( r, false ); - if( ei && !ei->d_constructor.get().isNull() && ei->d_constructor.get().getOperator()!=t.getOperator() ){ - Node deq = ei->d_constructor.get().eqNode( t ).negate(); - d_pending.push_back( deq ); - d_pending_exp[ deq ] = d_true; - Trace("datatypes-infer") << "DtInfer : diff constructor : " << deq << std::endl; - d_infer.push_back( deq ); - } - } - } - } -*/ - //d_consEqc[t] = true; } } @@ -865,14 +848,7 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){ if( d_conflict ){ return; } - //d_consEqc[t1] = true; } - //AJR: do this? - //else if( cons2.isConst() ){ - // //prefer the constant - // eqc1->d_constructor = cons2; - //} - //d_consEqc[t2] = false; } }else{ Trace("datatypes-debug") << " no eqc info for " << t1 << ", must create" << std::endl; @@ -1998,9 +1974,6 @@ Node TheoryDatatypes::searchForCycle( TNode n, TNode on, for( unsigned i=0; i<ncons.getNumChildren(); i++ ) { TNode cn = searchForCycle( ncons[i], on, visited, proc, explanation, false ); if( cn==on ) { - //if( Debug.isOn("datatypes-cycles") && !d_cycle_check.isConnectedNode( n, ncons[i] ) ){ - // Debug("datatypes-cycles") << "Cycle subterm: " << n << " is not -> " << ncons[i] << "!!!!" << std::endl; - //} //add explanation for why the constructor is connected if( n != ncons ) { explainEquality( n, ncons, true, explanation ); diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index e06bb7408..233ebd052 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -46,10 +46,6 @@ class TheoryDatatypes : public Theory { typedef context::CDHashMap<Node, bool, NodeHashFunction> BoolMap; typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeMap; - /** transitive closure to record equivalence/subterm relation. */ - // TransitiveClosureNode d_cycle_check; - /** has seen cycle */ - context::CDO<bool> d_hasSeenCycle; /** inferences */ NodeList d_infer; NodeList d_infer_exp; @@ -179,12 +175,19 @@ private: /** selector apps for eqch equivalence class */ NodeIntMap d_selector_apps; std::map< Node, std::vector< Node > > d_selector_apps_data; - /** constructor terms */ - //BoolMap d_consEqc; /** Are we in conflict */ context::CDO<bool> d_conflict; - /** Added lemma ? */ + /** added lemma + * + * This flag is set to true during a full effort check if this theory + * called d_out->lemma(...). + */ bool d_addedLemma; + /** added fact + * + * This flag is set to true during a full effort check if this theory + * added an internal fact to its equality engine. + */ bool d_addedFact; /** The conflict node */ Node d_conflictNode; diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp index 83098e3ba..3cf605238 100644 --- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp @@ -57,7 +57,7 @@ class CegInstantiatorBvInverterQuery : public BvInverterQuery }; BvInstantiator::BvInstantiator(QuantifiersEngine* qe, TypeNode tn) - : Instantiator(qe, tn) + : Instantiator(qe, tn), d_inst_id_counter(0) { // get the global inverter utility // this must be global since we need to: diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp index c281e81ca..ac76ee31f 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp @@ -38,11 +38,14 @@ using namespace CVC4::theory::arith; #define ARITH_INSTANTIATOR_USE_MINUS_DELTA -InstStrategyCbqi::InstStrategyCbqi( QuantifiersEngine * qe ) - : QuantifiersModule( qe ), d_added_cbqi_lemma( qe->getUserContext() ), -d_elim_quants( qe->getSatContext() ), -d_nested_qe_waitlist_size( qe->getUserContext() ), -d_nested_qe_waitlist_proc( qe->getUserContext() ) +InstStrategyCbqi::InstStrategyCbqi(QuantifiersEngine* qe) + : QuantifiersModule(qe), + d_cbqi_set_quant_inactive(false), + d_incomplete_check(false), + d_added_cbqi_lemma(qe->getUserContext()), + d_elim_quants(qe->getSatContext()), + d_nested_qe_waitlist_size(qe->getUserContext()), + d_nested_qe_waitlist_proc(qe->getUserContext()) //, d_added_inst( qe->getUserContext() ) { d_qid_count = 0; diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h index 236904ef2..4334652da 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h @@ -37,7 +37,18 @@ class InstStrategyCbqi : public QuantifiersModule { typedef context::CDHashMap< Node, int, NodeHashFunction> NodeIntMap; protected: + /** set quantified formula inactive + * + * This flag is set to true during a full effort check if at least one + * quantified formula is set "inactive", that is, its negation is + * unsatisfiable in the current context. + */ bool d_cbqi_set_quant_inactive; + /** incomplete check + * + * This is set to true during a full effort check if this strategy could + * not find an instantiation for at least one asserted quantified formula. + */ bool d_incomplete_check; /** whether we have added cbqi lemma */ NodeSet d_added_cbqi_lemma; diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index e82ab617a..a1c132fda 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -80,16 +80,18 @@ void OpArgIndex::getGroundTerms( ConjectureGenerator * s, std::vector< TNode >& } } - - -ConjectureGenerator::ConjectureGenerator( QuantifiersEngine * qe, context::Context* c ) : QuantifiersModule( qe ), -d_notify( *this ), -d_uequalityEngine(d_notify, c, "ConjectureGenerator::ee", false), -d_ee_conjectures( c ){ - d_fullEffortCount = 0; - d_conj_count = 0; - d_subs_confirmCount = 0; - d_subs_unkCount = 0; +ConjectureGenerator::ConjectureGenerator(QuantifiersEngine* qe, + context::Context* c) + : QuantifiersModule(qe), + d_notify(*this), + d_uequalityEngine(d_notify, c, "ConjectureGenerator::ee", false), + d_ee_conjectures(c), + d_conj_count(0), + d_subs_confirmCount(0), + d_subs_unkCount(0), + d_fullEffortCount(0), + d_hasAddedLemma(false) +{ d_uequalityEngine.addFunctionKind( kind::APPLY_UF ); d_uequalityEngine.addFunctionKind( kind::APPLY_CONSTRUCTOR ); diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h index 6d626038d..a3a0b8795 100644 --- a/src/theory/quantifiers/conjecture_generator.h +++ b/src/theory/quantifiers/conjecture_generator.h @@ -70,10 +70,19 @@ class TermGenEnv; class TermGenerator { -private: + private: unsigned calculateGeneralizationDepth( TermGenEnv * s, std::map< TypeNode, std::vector< int > >& fvs ); -public: - TermGenerator(){} + + public: + TermGenerator() + : d_id(0), + d_status(0), + d_status_num(0), + d_match_status(0), + d_match_status_child_num(0), + d_match_mode(0) + { + } TypeNode d_typ; unsigned d_id; //1 : consider as unique variable diff --git a/src/theory/quantifiers/ematching/candidate_generator.cpp b/src/theory/quantifiers/ematching/candidate_generator.cpp index 4208b11ae..6ea6e50b3 100644 --- a/src/theory/quantifiers/ematching/candidate_generator.cpp +++ b/src/theory/quantifiers/ematching/candidate_generator.cpp @@ -33,8 +33,9 @@ bool CandidateGenerator::isLegalCandidate( Node n ){ return d_qe->getTermDatabase()->isTermActive( n ) && ( !options::cbqi() || !quantifiers::TermUtil::hasInstConstAttr(n) ); } -CandidateGeneratorQE::CandidateGeneratorQE( QuantifiersEngine* qe, Node pat ) : -CandidateGenerator( qe ), d_term_iter( -1 ){ +CandidateGeneratorQE::CandidateGeneratorQE(QuantifiersEngine* qe, Node pat) + : CandidateGenerator(qe), d_term_iter(-1), d_term_iter_limit(0) +{ d_op = qe->getTermDatabase()->getMatchOperator( pat ); Assert( !d_op.isNull() ); } diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index a8079f775..1e3116f43 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -572,10 +572,6 @@ void FirstOrderModelIG::resetEvaluate(){ d_eval_uf_use_default.clear(); d_eval_uf_model.clear(); d_eval_term_index_order.clear(); - d_eval_formulas = 0; - d_eval_uf_terms = 0; - d_eval_lits = 0; - d_eval_lits_unknown = 0; } //if evaluate( n ) = eVal, @@ -585,7 +581,6 @@ void FirstOrderModelIG::resetEvaluate(){ // if eVal is not 0, then // each n{ri->d_index[0]/x_0...ri->d_index[depIndex]/x_depIndex, */x_(depIndex+1) ... */x_n } is equivalent in the current model int FirstOrderModelIG::evaluate( Node n, int& depIndex, RepSetIterator* ri ){ - ++d_eval_formulas; Debug("fmf-eval-debug2") << "Evaluate " << n << std::endl; //Notice() << "Eval " << n << std::endl; if( n.getKind()==NOT ){ @@ -661,7 +656,6 @@ int FirstOrderModelIG::evaluate( Node n, int& depIndex, RepSetIterator* ri ){ }else if( n.getKind()==FORALL ){ return 0; }else{ - ++d_eval_lits; //Debug("fmf-eval-debug") << "Evaluate literal " << n << std::endl; int retVal = 0; depIndex = ri->getNumTerms()-1; @@ -684,7 +678,6 @@ int FirstOrderModelIG::evaluate( Node n, int& depIndex, RepSetIterator* ri ){ if( retVal!=0 ){ Debug("fmf-eval-debug") << "Evaluate literal: return " << retVal << ", depIndex = " << depIndex << std::endl; }else{ - ++d_eval_lits_unknown; Trace("fmf-eval-amb") << "Neither true nor false : " << n << std::endl; Trace("fmf-eval-amb") << " value : " << val << std::endl; } @@ -731,7 +724,6 @@ Node FirstOrderModelIG::evaluateTerm( Node n, int& depIndex, RepSetIterator* ri //Debug("fmf-eval-debug") << "Evaluate term " << n << " (" << gn << ")" << std::endl; //if it is a defined UF, then consult the interpretation if( d_uf_model_tree.find( op )!=d_uf_model_tree.end() ){ - ++d_eval_uf_terms; int argDepIndex = 0; //make the term model specifically for n makeEvalUfModel( n ); diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index 059250f8d..7da5b2088 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -266,12 +266,6 @@ public: /** evaluate functions */ int evaluate( Node n, int& depIndex, RepSetIterator* ri ); Node evaluateTerm( Node n, int& depIndex, RepSetIterator* ri ); -public: - //statistics - int d_eval_formulas; - int d_eval_uf_terms; - int d_eval_lits; - int d_eval_lits_unknown; private: //default evaluate term function Node evaluateTermDefault( Node n, int& depIndex, std::vector< int >& childDepIndex, RepSetIterator* ri ); diff --git a/src/theory/quantifiers/fmf/model_builder.cpp b/src/theory/quantifiers/fmf/model_builder.cpp index d1b7eebb8..c03fc7a32 100644 --- a/src/theory/quantifiers/fmf/model_builder.cpp +++ b/src/theory/quantifiers/fmf/model_builder.cpp @@ -457,24 +457,17 @@ bool QModelBuilderIG::hasConstantDefinition( Node n ){ return false; } -QModelBuilderIG::Statistics::Statistics(): - d_num_quants_init("QModelBuilderIG::Number_Quantifiers", 0), - d_num_partial_quants_init("QModelBuilderIG::Number_Partial_Quantifiers", 0), - d_init_inst_gen_lemmas("QModelBuilderIG::Initialize_Inst_Gen_Lemmas", 0 ), - d_inst_gen_lemmas("QModelBuilderIG::Inst_Gen_Lemmas", 0 ), - d_eval_formulas("QModelBuilderIG::Eval_Formulas", 0 ), - d_eval_uf_terms("QModelBuilderIG::Eval_Uf_Terms", 0 ), - d_eval_lits("QModelBuilderIG::Eval_Lits", 0 ), - d_eval_lits_unknown("QModelBuilderIG::Eval_Lits_Unknown", 0 ) +QModelBuilderIG::Statistics::Statistics() + : d_num_quants_init("QModelBuilderIG::Number_Quantifiers", 0), + d_num_partial_quants_init("QModelBuilderIG::Number_Partial_Quantifiers", + 0), + d_init_inst_gen_lemmas("QModelBuilderIG::Initialize_Inst_Gen_Lemmas", 0), + d_inst_gen_lemmas("QModelBuilderIG::Inst_Gen_Lemmas", 0) { smtStatisticsRegistry()->registerStat(&d_num_quants_init); smtStatisticsRegistry()->registerStat(&d_num_partial_quants_init); smtStatisticsRegistry()->registerStat(&d_init_inst_gen_lemmas); smtStatisticsRegistry()->registerStat(&d_inst_gen_lemmas); - smtStatisticsRegistry()->registerStat(&d_eval_formulas); - smtStatisticsRegistry()->registerStat(&d_eval_uf_terms); - smtStatisticsRegistry()->registerStat(&d_eval_lits); - smtStatisticsRegistry()->registerStat(&d_eval_lits_unknown); } QModelBuilderIG::Statistics::~Statistics(){ @@ -482,10 +475,6 @@ QModelBuilderIG::Statistics::~Statistics(){ smtStatisticsRegistry()->unregisterStat(&d_num_partial_quants_init); smtStatisticsRegistry()->unregisterStat(&d_init_inst_gen_lemmas); smtStatisticsRegistry()->unregisterStat(&d_inst_gen_lemmas); - smtStatisticsRegistry()->unregisterStat(&d_eval_formulas); - smtStatisticsRegistry()->unregisterStat(&d_eval_uf_terms); - smtStatisticsRegistry()->unregisterStat(&d_eval_lits); - smtStatisticsRegistry()->unregisterStat(&d_eval_lits_unknown); } //do exhaustive instantiation @@ -558,12 +547,6 @@ int QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, in } } //print debugging information - if( fmig ){ - d_statistics.d_eval_formulas += fmig->d_eval_formulas; - d_statistics.d_eval_uf_terms += fmig->d_eval_uf_terms; - d_statistics.d_eval_lits += fmig->d_eval_lits; - d_statistics.d_eval_lits_unknown += fmig->d_eval_lits_unknown; - } Trace("inst-fmf-ei") << "For " << f << ", finished: " << std::endl; Trace("inst-fmf-ei") << " Inst Tried: " << d_triedLemmas << std::endl; Trace("inst-fmf-ei") << " Inst Added: " << d_addedLemmas << std::endl; diff --git a/src/theory/quantifiers/fmf/model_builder.h b/src/theory/quantifiers/fmf/model_builder.h index 353883a20..b34f1e580 100644 --- a/src/theory/quantifiers/fmf/model_builder.h +++ b/src/theory/quantifiers/fmf/model_builder.h @@ -148,10 +148,6 @@ class QModelBuilderIG : public QModelBuilder IntStat d_num_partial_quants_init; IntStat d_init_inst_gen_lemmas; IntStat d_inst_gen_lemmas; - IntStat d_eval_formulas; - IntStat d_eval_uf_terms; - IntStat d_eval_lits; - IntStat d_eval_lits_unknown; Statistics(); ~Statistics(); }; diff --git a/src/theory/quantifiers/macros.cpp b/src/theory/quantifiers/macros.cpp deleted file mode 100644 index d88f8eec9..000000000 --- a/src/theory/quantifiers/macros.cpp +++ /dev/null @@ -1,514 +0,0 @@ -/********************* */ -/*! \file macros.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Kshitij Bansal - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 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 Sort inference module - ** - ** This class implements quantifiers macro definitions. - **/ - -#include "theory/quantifiers/macros.h" - -#include <vector> - -#include "options/quantifiers_modes.h" -#include "options/quantifiers_options.h" -#include "proof/proof_manager.h" -#include "smt/smt_engine.h" -#include "smt/smt_engine_scope.h" -#include "theory/arith/arith_msum.h" -#include "theory/quantifiers/ematching/trigger.h" -#include "theory/quantifiers/term_database.h" -#include "theory/quantifiers/term_util.h" -#include "theory/rewriter.h" - -using namespace CVC4; -using namespace std; -using namespace CVC4::theory; -using namespace CVC4::theory::quantifiers; -using namespace CVC4::kind; - - -QuantifierMacros::QuantifierMacros( QuantifiersEngine * qe ) : d_qe( qe ){ - d_ground_macros = false; -} - -bool QuantifierMacros::simplify( std::vector< Node >& assertions, bool doRewrite ){ - unsigned rmax = options::macrosQuantMode()==MACROS_QUANT_MODE_ALL ? 2 : 1; - for( unsigned r=0; r<rmax; r++ ){ - d_ground_macros = (r==0); - Trace("macros") << "Find macros, ground=" << d_ground_macros << "..." << std::endl; - //first, collect macro definitions - std::vector< Node > macro_assertions; - for( int i=0; i<(int)assertions.size(); i++ ){ - Trace("macros-debug") << " process assertion " << assertions[i] << std::endl; - if( processAssertion( assertions[i] ) ){ - PROOF( - if( std::find( macro_assertions.begin(), macro_assertions.end(), assertions[i] )==macro_assertions.end() ){ - macro_assertions.push_back( assertions[i] ); - } - ); - //process this assertion again - i--; - } - } - Trace("macros") << "...finished process, #new def = " << d_macro_defs_new.size() << std::endl; - if( doRewrite && !d_macro_defs_new.empty() ){ - bool retVal = false; - Trace("macros") << "Do simplifications..." << std::endl; - //now, rewrite based on macro definitions - for( unsigned i=0; i<assertions.size(); i++ ){ - Node curr = simplify( assertions[i] ); - if( curr!=assertions[i] ){ - curr = Rewriter::rewrite( curr ); - Trace("macros-rewrite") << "Rewrite " << assertions[i] << " to " << curr << std::endl; - //for now, it is dependent upon all assertions involving macros, this is an over-approximation. - //a more fine-grained unsat core computation would require caching dependencies for each subterm of the formula, - // which is expensive. - PROOF( - ProofManager::currentPM()->addDependence(curr, assertions[i]); - for( unsigned j=0; j<macro_assertions.size(); j++ ){ - if( macro_assertions[j]!=assertions[i] ){ - ProofManager::currentPM()->addDependence(curr,macro_assertions[j]); - } - } - ); - assertions[i] = curr; - retVal = true; - } - } - d_macro_defs_new.clear(); - if( retVal ){ - return true; - } - } - } - if( Trace.isOn("macros-warn") ){ - for( unsigned i=0; i<assertions.size(); i++ ){ - debugMacroDefinition( assertions[i], assertions[i] ); - } - } - return false; -} - -bool QuantifierMacros::processAssertion( Node n ) { - if( n.getKind()==AND ){ - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - if( processAssertion( n[i] ) ){ - return true; - } - } - }else if( n.getKind()==FORALL && d_quant_macros.find( n )==d_quant_macros.end() ){ - std::vector< Node > args; - for( size_t j=0; j<n[0].getNumChildren(); j++ ){ - args.push_back( n[0][j] ); - } - Node nproc = n[1]; - if( !d_macro_defs_new.empty() ){ - nproc = simplify( nproc ); - if( nproc!=n[1] ){ - nproc = Rewriter::rewrite( nproc ); - } - } - //look at the body of the quantifier for macro definition - if( process( nproc, true, args, n ) ){ - d_quant_macros[n] = true; - return true; - } - } - return false; -} - -bool QuantifierMacros::containsBadOp( Node n, Node op, std::vector< Node >& opc, std::map< Node, bool >& visited ){ - if( visited.find( n )==visited.end() ){ - visited[n] = true; - if( n.getKind()==APPLY_UF ){ - Node nop = n.getOperator(); - if( nop==op || d_macro_defs.find( nop )!=d_macro_defs.end() ){ - return true; - } - if( std::find( opc.begin(), opc.end(), nop )==opc.end() ){ - opc.push_back( nop ); - } - }else if( d_ground_macros && n.getKind()==FORALL ){ - return true; - } - for( size_t i=0; i<n.getNumChildren(); i++ ){ - if( containsBadOp( n[i], op, opc, visited ) ){ - return true; - } - } - } - return false; -} - -bool QuantifierMacros::isMacroLiteral( Node n, bool pol ){ - return pol && n.getKind()==EQUAL; -} - -bool QuantifierMacros::isGroundUfTerm( Node f, Node n ) { - Node icn = d_qe->getTermUtil()->substituteBoundVariablesToInstConstants(n, f); - Trace("macros-debug2") << "Get free variables in " << icn << std::endl; - std::vector< Node > var; - quantifiers::TermUtil::computeInstConstContainsForQuant(f, icn, var); - Trace("macros-debug2") << "Get trigger variables for " << icn << std::endl; - std::vector< Node > trigger_var; - inst::Trigger::getTriggerVariables( icn, f, trigger_var ); - Trace("macros-debug2") << "Done." << std::endl; - //only if all variables are also trigger variables - return trigger_var.size()>=var.size(); -} - -bool QuantifierMacros::isBoundVarApplyUf( Node n ) { - Assert( n.getKind()==APPLY_UF ); - TypeNode tno = n.getOperator().getType(); - std::map< Node, bool > vars; - // allow if a vector of unique variables of the same type as UF arguments - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - if( n[i].getKind()!=BOUND_VARIABLE ){ - return false; - } - if( n[i].getType()!=tno[i] ){ - return false; - } - if( vars.find( n[i] )==vars.end() ){ - vars[n[i]] = true; - }else{ - return false; - } - } - return true; -} - -void QuantifierMacros::getMacroCandidates( Node n, std::vector< Node >& candidates, std::map< Node, bool >& visited ){ - if( visited.find( n )==visited.end() ){ - visited[n] = true; - if( n.getKind()==APPLY_UF ){ - if( isBoundVarApplyUf( n ) ){ - candidates.push_back( n ); - } - }else if( n.getKind()==PLUS ){ - for( size_t i=0; i<n.getNumChildren(); i++ ){ - getMacroCandidates( n[i], candidates, visited ); - } - }else if( n.getKind()==MULT ){ - //if the LHS is a constant - if( n.getNumChildren()==2 && n[0].isConst() ){ - getMacroCandidates( n[1], candidates, visited ); - } - }else if( n.getKind()==NOT ){ - getMacroCandidates( n[0], candidates, visited ); - } - } -} - -Node QuantifierMacros::solveInEquality( Node n, Node lit ){ - if( lit.getKind()==EQUAL ){ - //return the opposite side of the equality if defined that way - for( int i=0; i<2; i++ ){ - if( lit[i]==n ){ - return lit[i==0 ? 1 : 0]; - }else if( lit[i].getKind()==NOT && lit[i][0]==n ){ - return lit[i==0 ? 1 : 0].negate(); - } - } - std::map<Node, Node> msum; - if (ArithMSum::getMonomialSumLit(lit, msum)) - { - Node veq_c; - Node val; - int res = ArithMSum::isolate(n, msum, veq_c, val, EQUAL); - if (res != 0 && veq_c.isNull()) - { - return val; - } - } - } - Trace("macros-debug") << "Cannot find for " << lit << " " << n << std::endl; - return Node::null(); -} - -bool QuantifierMacros::getFreeVariables( Node n, std::vector< Node >& v_quant, std::vector< Node >& vars, bool retOnly, std::map< Node, bool >& visited ){ - if( visited.find( n )==visited.end() ){ - visited[n] = true; - if( std::find( v_quant.begin(), v_quant.end(), n )!=v_quant.end() ){ - if( std::find( vars.begin(), vars.end(), n )==vars.end() ){ - if( retOnly ){ - return true; - }else{ - vars.push_back( n ); - } - } - } - for( size_t i=0; i<n.getNumChildren(); i++ ){ - if( getFreeVariables( n[i], v_quant, vars, retOnly, visited ) ){ - return true; - } - } - } - return false; -} - -bool QuantifierMacros::getSubstitution( std::vector< Node >& v_quant, std::map< Node, Node >& solved, - std::vector< Node >& vars, std::vector< Node >& subs, bool reqComplete ){ - bool success = true; - for( size_t a=0; a<v_quant.size(); a++ ){ - if( !solved[ v_quant[a] ].isNull() ){ - vars.push_back( v_quant[a] ); - subs.push_back( solved[ v_quant[a] ] ); - }else{ - if( reqComplete ){ - success = false; - break; - } - } - } - return success; -} - -bool QuantifierMacros::process( Node n, bool pol, std::vector< Node >& args, Node f ){ - Trace("macros-debug") << " process " << n << std::endl; - if( n.getKind()==NOT ){ - return process( n[0], !pol, args, f ); - }else if( n.getKind()==AND || n.getKind()==OR ){ - //bool favorPol = (n.getKind()==AND)==pol; - //conditional? - }else if( n.getKind()==ITE ){ - //can not do anything - }else if( n.getKind()==APPLY_UF ){ - //predicate case - if( isBoundVarApplyUf( n ) ){ - Node op = n.getOperator(); - if( d_macro_defs.find( op )==d_macro_defs.end() ){ - Node n_def = NodeManager::currentNM()->mkConst( pol ); - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - std::stringstream ss; - ss << "mda_" << op << ""; - Node v = NodeManager::currentNM()->mkSkolem( ss.str(), n[i].getType(), "created during macro definition recognition" ); - d_macro_basis[op].push_back( v ); - } - //contains no ops - std::vector< Node > op_contains; - //add the macro - addMacro( op, n_def, op_contains ); - return true; - } - } - }else{ - //literal case - if( isMacroLiteral( n, pol ) ){ - Trace("macros-debug") << "Check macro literal : " << n << std::endl; - std::map< Node, bool > visited; - std::vector< Node > candidates; - for( size_t i=0; i<n.getNumChildren(); i++ ){ - getMacroCandidates( n[i], candidates, visited ); - } - for( size_t i=0; i<candidates.size(); i++ ){ - Node m = candidates[i]; - Node op = m.getOperator(); - Trace("macros-debug") << "Check macro candidate : " << m << std::endl; - if( d_macro_defs.find( op )==d_macro_defs.end() ){ - std::vector< Node > fvs; - visited.clear(); - getFreeVariables( m, args, fvs, false, visited ); - //get definition and condition - Node n_def = solveInEquality( m, n ); //definition for the macro - if( !n_def.isNull() ){ - Trace("macros-debug") << m << " is possible macro in " << f << std::endl; - Trace("macros-debug") << " corresponding definition is : " << n_def << std::endl; - visited.clear(); - //definition must exist and not contain any free variables apart from fvs - if( !getFreeVariables( n_def, args, fvs, true, visited ) ){ - Trace("macros-debug") << "...free variables are contained." << std::endl; - visited.clear(); - //cannot contain a defined operator, opc is list of functions it contains - std::vector< Node > opc; - if( !containsBadOp( n_def, op, opc, visited ) ){ - Trace("macros-debug") << "...does not contain bad (recursive) operator." << std::endl; - //must be ground UF term if mode is GROUND_UF - if( options::macrosQuantMode()!=MACROS_QUANT_MODE_GROUND_UF || isGroundUfTerm( f, n_def ) ){ - Trace("macros-debug") << "...respects ground-uf constraint." << std::endl; - //now we must rewrite candidates[i] to a term of form g( x1, ..., xn ) where - // x1 ... xn are distinct variables - if( d_macro_basis[op].empty() ){ - for( size_t a=0; a<m.getNumChildren(); a++ ){ - std::stringstream ss; - ss << "mda_" << op << ""; - Node v = NodeManager::currentNM()->mkSkolem( ss.str(), m[a].getType(), "created during macro definition recognition" ); - d_macro_basis[op].push_back( v ); - } - } - std::map< Node, Node > solved; - for( size_t a=0; a<m.getNumChildren(); a++ ){ - solved[m[a]] = d_macro_basis[op][a]; - } - std::vector< Node > vars; - std::vector< Node > subs; - if( getSubstitution( fvs, solved, vars, subs, true ) ){ - n_def = n_def.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); - addMacro( op, n_def, opc ); - return true; - } - } - } - } - } - } - } - } - } - return false; -} - -Node QuantifierMacros::simplify( Node n ){ - if( n.getNumChildren()==0 ){ - return n; - }else{ - std::map< Node, Node >::iterator itn = d_simplify_cache.find( n ); - if( itn!=d_simplify_cache.end() ){ - return itn->second; - }else{ - Node ret = n; - Trace("macros-debug") << " simplify " << n << std::endl; - std::vector< Node > children; - bool childChanged = false; - for( size_t i=0; i<n.getNumChildren(); i++ ){ - Node nn = simplify( n[i] ); - children.push_back( nn ); - childChanged = childChanged || nn!=n[i]; - } - bool retSet = false; - if( n.getKind()==APPLY_UF ){ - Node op = n.getOperator(); - std::map< Node, Node >::iterator it = d_macro_defs.find( op ); - if( it!=d_macro_defs.end() && !it->second.isNull() ){ - //only apply if children are subtypes of arguments - bool success = true; - // FIXME : this can be eliminated when we have proper typing rules - std::vector< Node > cond; - TypeNode tno = op.getType(); - for( unsigned i=0; i<children.size(); i++ ){ - Node etc = TypeNode::getEnsureTypeCondition( children[i], tno[i] ); - if( etc.isNull() ){ - //if this does fail, we are incomplete, since we are eliminating quantified formula corresponding to op, - // and not ensuring it applies to n when its types are correct. - //Assert( false ); - success = false; - break; - }else if( !etc.isConst() ){ - cond.push_back( etc ); - } - Assert( children[i].getType().isSubtypeOf( tno[i] ) ); - } - if( success ){ - //do substitution if necessary - ret = it->second; - std::map< Node, std::vector< Node > >::iterator itb = d_macro_basis.find( op ); - if( itb!=d_macro_basis.end() ){ - ret = ret.substitute( itb->second.begin(), itb->second.end(), children.begin(), children.end() ); - } - if( !cond.empty() ){ - Node cc = cond.size()==1 ? cond[0] : NodeManager::currentNM()->mkNode( kind::AND, cond ); - ret = NodeManager::currentNM()->mkNode( kind::ITE, cc, ret, n ); - } - retSet = true; - } - } - } - if( !retSet && childChanged ){ - if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){ - children.insert( children.begin(), n.getOperator() ); - } - ret = NodeManager::currentNM()->mkNode( n.getKind(), children ); - } - d_simplify_cache[n] = ret; - return ret; - } - } -} - -void QuantifierMacros::debugMacroDefinition( Node oo, Node n ) { - //for debugging, ensure that all previous definitions have been eliminated - if( n.getKind()==APPLY_UF ){ - Node op = n.getOperator(); - if( d_macro_defs.find( op )!=d_macro_defs.end() ){ - if( d_macro_defs.find( oo )!=d_macro_defs.end() ){ - Trace("macros-warn") << "BAD DEFINITION for macro " << oo << " : " << d_macro_defs[oo] << std::endl; - }else{ - Trace("macros-warn") << "BAD ASSERTION " << oo << std::endl; - } - Trace("macros-warn") << " contains defined function " << op << "!!!" << std::endl; - } - } - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - debugMacroDefinition( oo, n[i] ); - } -} - -void QuantifierMacros::finalizeDefinitions() { - bool doDefs = false; - if( Trace.isOn("macros-warn") ){ - doDefs = true; - } - if( options::incrementalSolving() || options::produceModels() || doDefs ){ - Trace("macros") << "Store as defined functions..." << std::endl; - //also store as defined functions - for( std::map< Node, Node >::iterator it = d_macro_defs.begin(); it != d_macro_defs.end(); ++it ){ - Trace("macros-def") << "Macro definition for " << it->first << " : " << it->second << std::endl; - Trace("macros-def") << " basis is : "; - std::vector< Node > nargs; - std::vector< Expr > args; - for( unsigned i=0; i<d_macro_basis[it->first].size(); i++ ){ - Node bv = NodeManager::currentNM()->mkBoundVar( d_macro_basis[it->first][i].getType() ); - Trace("macros-def") << d_macro_basis[it->first][i] << " "; - nargs.push_back( bv ); - args.push_back( bv.toExpr() ); - } - Trace("macros-def") << std::endl; - Node sbody = it->second.substitute( d_macro_basis[it->first].begin(), d_macro_basis[it->first].end(), nargs.begin(), nargs.end() ); - smt::currentSmtEngine()->defineFunction( it->first.toExpr(), args, sbody.toExpr() ); - - if( Trace.isOn("macros-warn") ){ - debugMacroDefinition( it->first, sbody ); - } - } - Trace("macros") << "done." << std::endl; - } -} - -void QuantifierMacros::addMacro( Node op, Node n, std::vector< Node >& opc ) { - Trace("macros") << "* " << n << " is a macro for " << op << ", #op contain = " << opc.size() << std::endl; - d_simplify_cache.clear(); - d_macro_defs[op] = n; - d_macro_defs_new[op] = n; - //substitute into all previous - std::vector< Node > dep_ops; - dep_ops.push_back( op ); - Trace("macros-debug") << "...substitute into " << d_macro_def_contains[op].size() << " previous definitions." << std::endl; - for( unsigned i=0; i<d_macro_def_contains[op].size(); i++ ){ - Node cop = d_macro_def_contains[op][i]; - Node def = d_macro_defs[cop]; - def = simplify( def ); - d_macro_defs[cop] = def; - if( d_macro_defs_new.find( cop )!=d_macro_defs_new.end() ){ - d_macro_defs_new[cop] = def; - } - dep_ops.push_back( cop ); - } - //store the contains op information - for( unsigned i=0; i<opc.size(); i++ ){ - for( unsigned j=0; j<dep_ops.size(); j++ ){ - Node dop = dep_ops[j]; - if( std::find( d_macro_def_contains[opc[i]].begin(), d_macro_def_contains[opc[i]].end(), dop )==d_macro_def_contains[opc[i]].end() ){ - d_macro_def_contains[opc[i]].push_back( dop ); - } - } - } -} diff --git a/src/theory/quantifiers/macros.h b/src/theory/quantifiers/macros.h deleted file mode 100644 index b36be7aec..000000000 --- a/src/theory/quantifiers/macros.h +++ /dev/null @@ -1,74 +0,0 @@ -/********************* */ -/*! \file macros.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 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 Pre-process step for detecting quantifier macro definitions - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__QUANTIFIERS_MACROS_H -#define __CVC4__QUANTIFIERS_MACROS_H - -#include <iostream> -#include <string> -#include <vector> -#include <map> -#include "expr/node.h" -#include "expr/type_node.h" -#include "theory/quantifiers_engine.h" - -namespace CVC4 { -namespace theory { -namespace quantifiers { - -class QuantifierMacros{ -private: - QuantifiersEngine * d_qe; -private: - bool d_ground_macros; - bool processAssertion( Node n ); - bool isBoundVarApplyUf( Node n ); - bool process( Node n, bool pol, std::vector< Node >& args, Node f ); - bool containsBadOp( Node n, Node op, std::vector< Node >& opc, std::map< Node, bool >& visited ); - bool isMacroLiteral( Node n, bool pol ); - bool isGroundUfTerm( Node f, Node n ); - void getMacroCandidates( Node n, std::vector< Node >& candidates, std::map< Node, bool >& visited ); - Node solveInEquality( Node n, Node lit ); - bool getFreeVariables( Node n, std::vector< Node >& v_quant, std::vector< Node >& vars, bool retOnly, std::map< Node, bool >& visited ); - bool getSubstitution( std::vector< Node >& v_quant, std::map< Node, Node >& solved, - std::vector< Node >& vars, std::vector< Node >& subs, bool reqComplete ); - //map from operators to macro basis terms - std::map< Node, std::vector< Node > > d_macro_basis; - //map from operators to macro definition - std::map< Node, Node > d_macro_defs; - std::map< Node, Node > d_macro_defs_new; - //operators to macro ops that contain them - std::map< Node, std::vector< Node > > d_macro_def_contains; - //simplify caches - std::map< Node, Node > d_simplify_cache; - std::map< Node, bool > d_quant_macros; -private: - Node simplify( Node n ); - void addMacro( Node op, Node n, std::vector< Node >& opc ); - void debugMacroDefinition( Node oo, Node n ); -public: - QuantifierMacros( QuantifiersEngine * qe ); - ~QuantifierMacros(){} - - bool simplify( std::vector< Node >& assertions, bool doRewrite = false ); - void finalizeDefinitions(); -}; - -} -} -} - -#endif diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index a5cd95d29..510953035 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -70,10 +70,36 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* u, TheoryEngine* te) : d_te(te), + d_eq_query(new quantifiers::EqualityQueryQuantifiersEngine(c, this)), + d_eq_inference(nullptr), + d_inst_prop(nullptr), + d_tr_trie(new inst::TriggerTrie), + d_model(nullptr), + d_quant_rel(nullptr), + d_rel_dom(nullptr), + d_bv_invert(nullptr), + d_builder(nullptr), + d_qepr(nullptr), + d_term_util(new quantifiers::TermUtil(this)), + d_term_db(new quantifiers::TermDb(c, u, this)), + d_sygus_tdb(nullptr), d_quant_attr(new quantifiers::QuantAttributes(this)), d_instantiate(new quantifiers::Instantiate(this, u)), d_skolemize(new quantifiers::Skolemize(this, u)), d_term_enum(new quantifiers::TermEnumeration), + d_alpha_equiv(nullptr), + d_inst_engine(nullptr), + d_model_engine(nullptr), + d_bint(nullptr), + d_qcf(nullptr), + d_rr_engine(nullptr), + d_sg_gen(nullptr), + d_ceg_inst(nullptr), + d_lte_part_inst(nullptr), + d_fs(nullptr), + d_i_cbqi(nullptr), + d_qsplit(nullptr), + d_anti_skolem(nullptr), d_conflict_c(c, false), // d_quants(u), d_quants_prereg(u), @@ -89,41 +115,29 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, d_presolve_cache_wq(u), d_presolve_cache_wic(u) { - //utilities - d_eq_query = new quantifiers::EqualityQueryQuantifiersEngine( c, this ); - d_util.push_back( d_eq_query ); + //---- utilities + d_util.push_back(d_eq_query.get()); + // term util must come before the other utilities + d_util.push_back(d_term_util.get()); + d_util.push_back(d_term_db.get()); - // term util must come first - d_term_util = new quantifiers::TermUtil(this); - d_util.push_back(d_term_util); - - d_term_db = new quantifiers::TermDb( c, u, this ); - d_util.push_back( d_term_db ); - if (options::ceGuidedInst()) { - d_sygus_tdb = new quantifiers::TermDbSygus(c, this); - }else{ - d_sygus_tdb = NULL; + d_sygus_tdb.reset(new quantifiers::TermDbSygus(c, this)); } if( options::instPropagate() ){ // notice that this option is incompatible with options::qcfAllConflict() - d_inst_prop = new quantifiers::InstPropagator( this ); - d_util.push_back( d_inst_prop ); + d_inst_prop.reset(new quantifiers::InstPropagator(this)); + d_util.push_back(d_inst_prop.get()); d_instantiate->addNotify(d_inst_prop->getInstantiationNotify()); - }else{ - d_inst_prop = NULL; } if( options::inferArithTriggerEq() ){ - d_eq_inference = new quantifiers::EqualityInference(c, false); - }else{ - d_eq_inference = NULL; + d_eq_inference.reset(new quantifiers::EqualityInference(c, false)); } d_util.push_back(d_instantiate.get()); - d_tr_trie = new inst::TriggerTrie; d_curr_effort_level = QuantifiersModule::QEFFORT_NONE; d_conflict = false; d_hasAddedLemma = false; @@ -135,37 +149,15 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, Trace("quant-engine-debug") << "Initialize model, mbqi : " << options::mbqiMode() << std::endl; if( options::relevantTriggers() ){ - d_quant_rel = new quantifiers::QuantRelevance; - d_util.push_back(d_quant_rel); - }else{ - d_quant_rel = NULL; + d_quant_rel.reset(new quantifiers::QuantRelevance); + d_util.push_back(d_quant_rel.get()); } if( options::quantEpr() ){ Assert( !options::incrementalSolving() ); - d_qepr = new quantifiers::QuantEPR; - }else{ - d_qepr = NULL; + d_qepr.reset(new quantifiers::QuantEPR); } - - - d_qcf = NULL; - d_sg_gen = NULL; - d_inst_engine = NULL; - d_i_cbqi = NULL; - d_qsplit = NULL; - d_anti_skolem = NULL; - d_model = NULL; - d_model_engine = NULL; - d_bint = NULL; - d_rr_engine = NULL; - d_ceg_inst = NULL; - d_lte_part_inst = NULL; - d_alpha_equiv = NULL; - d_fs = NULL; - d_rel_dom = NULL; - d_bv_invert = NULL; - d_builder = NULL; + //---- end utilities //allow theory combination to go first, once initially d_ierCounter = options::instWhenTcFirst() ? 0 : 1; @@ -178,70 +170,70 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, bool needsRelDom = false; //add quantifiers modules if( options::quantConflictFind() || options::quantRewriteRules() ){ - d_qcf = new quantifiers::QuantConflictFind( this, c); - d_modules.push_back( d_qcf ); + d_qcf.reset(new quantifiers::QuantConflictFind(this, c)); + d_modules.push_back(d_qcf.get()); } if( options::conjectureGen() ){ - d_sg_gen = new quantifiers::ConjectureGenerator( this, c ); - d_modules.push_back( d_sg_gen ); + d_sg_gen.reset(new quantifiers::ConjectureGenerator(this, c)); + d_modules.push_back(d_sg_gen.get()); } if( !options::finiteModelFind() || options::fmfInstEngine() ){ - d_inst_engine = new quantifiers::InstantiationEngine( this ); - d_modules.push_back( d_inst_engine ); + d_inst_engine.reset(new quantifiers::InstantiationEngine(this)); + d_modules.push_back(d_inst_engine.get()); } if( options::cbqi() ){ - d_i_cbqi = new quantifiers::InstStrategyCegqi( this ); - d_modules.push_back( d_i_cbqi ); + d_i_cbqi.reset(new quantifiers::InstStrategyCegqi(this)); + d_modules.push_back(d_i_cbqi.get()); if( options::cbqiBv() ){ // if doing instantiation for BV, need the inverter class - d_bv_invert = new quantifiers::BvInverter; + d_bv_invert.reset(new quantifiers::BvInverter); } } if( options::ceGuidedInst() ){ - d_ceg_inst = new quantifiers::CegInstantiation( this, c ); - d_modules.push_back( d_ceg_inst ); + d_ceg_inst.reset(new quantifiers::CegInstantiation(this, c)); + d_modules.push_back(d_ceg_inst.get()); //needsBuilder = true; } //finite model finding if( options::finiteModelFind() ){ if( options::fmfBound() ){ - d_bint = new quantifiers::BoundedIntegers( c, this ); - d_modules.push_back( d_bint ); + d_bint.reset(new quantifiers::BoundedIntegers(c, this)); + d_modules.push_back(d_bint.get()); } - d_model_engine = new quantifiers::ModelEngine( c, this ); - d_modules.push_back( d_model_engine ); + d_model_engine.reset(new quantifiers::ModelEngine(c, this)); + d_modules.push_back(d_model_engine.get()); //finite model finder has special ways of building the model needsBuilder = true; } if( options::quantRewriteRules() ){ - d_rr_engine = new quantifiers::RewriteEngine( c, this ); - d_modules.push_back(d_rr_engine); + d_rr_engine.reset(new quantifiers::RewriteEngine(c, this)); + d_modules.push_back(d_rr_engine.get()); } if( options::ltePartialInst() ){ - d_lte_part_inst = new quantifiers::LtePartialInst( this, c ); - d_modules.push_back( d_lte_part_inst ); + d_lte_part_inst.reset(new quantifiers::LtePartialInst(this, c)); + d_modules.push_back(d_lte_part_inst.get()); } if( options::quantDynamicSplit()!=quantifiers::QUANT_DSPLIT_MODE_NONE ){ - d_qsplit = new quantifiers::QuantDSplit( this, c ); - d_modules.push_back( d_qsplit ); + d_qsplit.reset(new quantifiers::QuantDSplit(this, c)); + d_modules.push_back(d_qsplit.get()); } if( options::quantAntiSkolem() ){ - d_anti_skolem = new quantifiers::QuantAntiSkolem( this ); - d_modules.push_back( d_anti_skolem ); + d_anti_skolem.reset(new quantifiers::QuantAntiSkolem(this)); + d_modules.push_back(d_anti_skolem.get()); } if( options::quantAlphaEquiv() ){ - d_alpha_equiv = new quantifiers::AlphaEquivalence( this ); + d_alpha_equiv.reset(new quantifiers::AlphaEquivalence(this)); } //full saturation : instantiate from relevant domain, then arbitrary terms if( options::fullSaturateQuant() || options::fullSaturateInterleave() ){ - d_fs = new quantifiers::InstStrategyEnum(this); - d_modules.push_back( d_fs ); + d_fs.reset(new quantifiers::InstStrategyEnum(this)); + d_modules.push_back(d_fs.get()); needsRelDom = true; } if( needsRelDom ){ - d_rel_dom = new quantifiers::RelevantDomain( this ); - d_util.push_back( d_rel_dom ); + d_rel_dom.reset(new quantifiers::RelevantDomain(this)); + d_util.push_back(d_rel_dom.get()); } // if we require specialized ways of building the model @@ -252,53 +244,27 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, || options::fmfBound()) { Trace("quant-engine-debug") << "...make fmc builder." << std::endl; - d_model = new quantifiers::fmcheck::FirstOrderModelFmc( this, c, "FirstOrderModelFmc" ); - d_builder = new quantifiers::fmcheck::FullModelChecker( c, this ); + d_model.reset(new quantifiers::fmcheck::FirstOrderModelFmc( + this, c, "FirstOrderModelFmc")); + d_builder.reset(new quantifiers::fmcheck::FullModelChecker(c, this)); }else if( options::mbqiMode()==quantifiers::MBQI_ABS ){ Trace("quant-engine-debug") << "...make abs mbqi builder." << std::endl; - d_model = new quantifiers::FirstOrderModelAbs( this, c, "FirstOrderModelAbs" ); - d_builder = new quantifiers::AbsMbqiBuilder( c, this ); + d_model.reset( + new quantifiers::FirstOrderModelAbs(this, c, "FirstOrderModelAbs")); + d_builder.reset(new quantifiers::AbsMbqiBuilder(c, this)); }else{ Trace("quant-engine-debug") << "...make default model builder." << std::endl; - d_model = new quantifiers::FirstOrderModelIG( this, c, "FirstOrderModelIG" ); - d_builder = new quantifiers::QModelBuilderDefault( c, this ); + d_model.reset( + new quantifiers::FirstOrderModelIG(this, c, "FirstOrderModelIG")); + d_builder.reset(new quantifiers::QModelBuilderDefault(c, this)); } }else{ - d_model = new quantifiers::FirstOrderModelIG( this, c, "FirstOrderModelIG" ); + d_model.reset( + new quantifiers::FirstOrderModelIG(this, c, "FirstOrderModelIG")); } } -QuantifiersEngine::~QuantifiersEngine() -{ - delete d_alpha_equiv; - delete d_builder; - delete d_qepr; - delete d_rr_engine; - delete d_bint; - delete d_model_engine; - delete d_inst_engine; - delete d_qcf; - delete d_quant_rel; - delete d_rel_dom; - delete d_bv_invert; - delete d_model; - delete d_tr_trie; - delete d_term_db; - delete d_sygus_tdb; - delete d_term_util; - delete d_eq_inference; - delete d_eq_query; - delete d_sg_gen; - delete d_ceg_inst; - delete d_lte_part_inst; - delete d_fs; - delete d_i_cbqi; - delete d_qsplit; - delete d_anti_skolem; - delete d_inst_prop; -} - -EqualityQuery* QuantifiersEngine::getEqualityQuery() { return d_eq_query; } +QuantifiersEngine::~QuantifiersEngine() {} context::Context* QuantifiersEngine::getSatContext() { @@ -325,6 +291,96 @@ const LogicInfo& QuantifiersEngine::getLogicInfo() const return d_te->getLogicInfo(); } +EqualityQuery* QuantifiersEngine::getEqualityQuery() const +{ + return d_eq_query.get(); +} +quantifiers::EqualityInference* QuantifiersEngine::getEqualityInference() const +{ + return d_eq_inference.get(); +} +quantifiers::RelevantDomain* QuantifiersEngine::getRelevantDomain() const +{ + return d_rel_dom.get(); +} +quantifiers::BvInverter* QuantifiersEngine::getBvInverter() const +{ + return d_bv_invert.get(); +} +quantifiers::QuantRelevance* QuantifiersEngine::getQuantifierRelevance() const +{ + return d_quant_rel.get(); +} +quantifiers::QModelBuilder* QuantifiersEngine::getModelBuilder() const +{ + return d_builder.get(); +} +quantifiers::QuantEPR* QuantifiersEngine::getQuantEPR() const +{ + return d_qepr.get(); +} +quantifiers::FirstOrderModel* QuantifiersEngine::getModel() const +{ + return d_model.get(); +} +quantifiers::TermDb* QuantifiersEngine::getTermDatabase() const +{ + return d_term_db.get(); +} +quantifiers::TermDbSygus* QuantifiersEngine::getTermDatabaseSygus() const +{ + return d_sygus_tdb.get(); +} +quantifiers::TermUtil* QuantifiersEngine::getTermUtil() const +{ + return d_term_util.get(); +} +quantifiers::QuantAttributes* QuantifiersEngine::getQuantAttributes() const +{ + return d_quant_attr.get(); +} +quantifiers::Instantiate* QuantifiersEngine::getInstantiate() const +{ + return d_instantiate.get(); +} +quantifiers::Skolemize* QuantifiersEngine::getSkolemize() const +{ + return d_skolemize.get(); +} +quantifiers::TermEnumeration* QuantifiersEngine::getTermEnumeration() const +{ + return d_term_enum.get(); +} +inst::TriggerTrie* QuantifiersEngine::getTriggerDatabase() const +{ + return d_tr_trie.get(); +} + +quantifiers::BoundedIntegers* QuantifiersEngine::getBoundedIntegers() const +{ + return d_bint.get(); +} +quantifiers::QuantConflictFind* QuantifiersEngine::getConflictFind() const +{ + return d_qcf.get(); +} +quantifiers::RewriteEngine* QuantifiersEngine::getRewriteEngine() const +{ + return d_rr_engine.get(); +} +quantifiers::CegInstantiation* QuantifiersEngine::getCegInstantiation() const +{ + return d_ceg_inst.get(); +} +quantifiers::InstStrategyEnum* QuantifiersEngine::getInstStrategyEnum() const +{ + return d_fs.get(); +} +quantifiers::InstStrategyCbqi* QuantifiersEngine::getInstStrategyCbqi() const +{ + return d_i_cbqi.get(); +} + QuantifiersModule * QuantifiersEngine::getOwner( Node q ) { std::map< Node, QuantifiersModule * >::iterator it = d_owner.find( q ); if( it==d_owner.end() ){ @@ -419,7 +475,8 @@ void QuantifiersEngine::check( Theory::Effort e ){ // if we want to use the model's equality engine, build the model now if( d_useModelEe && !d_model->isBuilt() ){ Trace("quant-engine-debug") << "Build the model." << std::endl; - if( !d_te->getModelBuilder()->buildModel( d_model ) ){ + if (!d_te->getModelBuilder()->buildModel(d_model.get())) + { //we are done if model building was unsuccessful flushLemmas(); if( d_hasAddedLemma ){ @@ -582,9 +639,10 @@ void QuantifiersEngine::check( Theory::Effort e ){ { // theory engine's model builder is quantifier engine's builder if it // has one - Assert(!d_builder || d_builder == d_te->getModelBuilder()); + Assert(!getModelBuilder() + || getModelBuilder() == d_te->getModelBuilder()); Trace("quant-engine-debug") << "Build model..." << std::endl; - if (!d_te->getModelBuilder()->buildModel(d_model)) + if (!d_te->getModelBuilder()->buildModel(d_model.get())) { flushLemmas(); } diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 674954023..aabca1640 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -84,134 +84,17 @@ namespace inst { class QuantifiersEngine { - // TODO: remove these github issue #1163 - friend class quantifiers::InstantiationEngine; - friend class quantifiers::InstStrategyCbqi; - friend class quantifiers::InstStrategyCegqi; - friend class quantifiers::ModelEngine; - friend class quantifiers::RewriteEngine; - friend class quantifiers::QuantConflictFind; - friend class inst::InstMatch; typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap; typedef context::CDList<Node> NodeList; typedef context::CDList<bool> BoolList; typedef context::CDHashSet<Node, NodeHashFunction> NodeSet; -private: - /** reference to theory engine object */ - TheoryEngine* d_te; - /** vector of utilities for quantifiers */ - std::vector< QuantifiersUtil* > d_util; - /** vector of modules for quantifiers */ - std::vector< QuantifiersModule* > d_modules; - /** equality query class */ - quantifiers::EqualityQueryQuantifiersEngine* d_eq_query; - /** equality inference class */ - quantifiers::EqualityInference* d_eq_inference; - /** for computing relevance of quantifiers */ - quantifiers::QuantRelevance* d_quant_rel; - /** relevant domain */ - quantifiers::RelevantDomain* d_rel_dom; - /** inversion utility for BV instantiation */ - quantifiers::BvInverter * d_bv_invert; - /** alpha equivalence */ - quantifiers::AlphaEquivalence * d_alpha_equiv; - /** model builder */ - quantifiers::QModelBuilder* d_builder; - /** utility for effectively propositional logic */ - quantifiers::QuantEPR* d_qepr; - /** term database */ - quantifiers::TermDb* d_term_db; - /** sygus term database */ - quantifiers::TermDbSygus* d_sygus_tdb; - /** term utilities */ - quantifiers::TermUtil* d_term_util; - /** quantifiers attributes */ - std::unique_ptr<quantifiers::QuantAttributes> d_quant_attr; - /** instantiate utility */ - std::unique_ptr<quantifiers::Instantiate> d_instantiate; - /** skolemize utility */ - std::unique_ptr<quantifiers::Skolemize> d_skolemize; - /** term enumeration utility */ - std::unique_ptr<quantifiers::TermEnumeration> d_term_enum; - /** instantiation engine */ - quantifiers::InstantiationEngine* d_inst_engine; - /** model engine */ - quantifiers::ModelEngine* d_model_engine; - /** bounded integers utility */ - quantifiers::BoundedIntegers * d_bint; - /** Conflict find mechanism for quantifiers */ - quantifiers::QuantConflictFind* d_qcf; - /** rewrite rules utility */ - quantifiers::RewriteEngine * d_rr_engine; - /** subgoal generator */ - quantifiers::ConjectureGenerator * d_sg_gen; - /** ceg instantiation */ - quantifiers::CegInstantiation * d_ceg_inst; - /** lte partial instantiation */ - quantifiers::LtePartialInst * d_lte_part_inst; - /** full saturation */ - quantifiers::InstStrategyEnum* d_fs; - /** counterexample-based quantifier instantiation */ - quantifiers::InstStrategyCbqi * d_i_cbqi; - /** quantifiers splitting */ - quantifiers::QuantDSplit * d_qsplit; - /** quantifiers anti-skolemization */ - quantifiers::QuantAntiSkolem * d_anti_skolem; - /** quantifiers instantiation propagtor */ - quantifiers::InstPropagator * d_inst_prop; - - private: //this information is reset during check - /** current effort level */ - QuantifiersModule::QEffort d_curr_effort_level; - /** are we in conflict */ - bool d_conflict; - context::CDO<bool> d_conflict_c; - /** has added lemma this round */ - bool d_hasAddedLemma; - /** whether to use model equality engine */ - bool d_useModelEe; - private: - /** list of all quantifiers seen */ - std::map< Node, bool > d_quants; - /** quantifiers pre-registered */ - NodeSet d_quants_prereg; - /** quantifiers reduced */ - BoolMap d_quants_red; - std::map< Node, Node > d_quants_red_lem; - /** list of all lemmas produced */ - //std::map< Node, bool > d_lemmas_produced; - BoolMap d_lemmas_produced_c; - /** lemmas waiting */ - std::vector< Node > d_lemmas_waiting; - /** phase requirements waiting */ - std::map< Node, bool > d_phase_req_waiting; - /** all triggers will be stored in this trie */ - inst::TriggerTrie* d_tr_trie; - /** extended model object */ - quantifiers::FirstOrderModel* d_model; - /** inst round counters TODO: make context-dependent? */ - context::CDO< int > d_ierCounter_c; - int d_ierCounter; - int d_ierCounter_lc; - int d_ierCounterLastLc; - int d_inst_when_phase; - /** has presolve been called */ - context::CDO< bool > d_presolve; - /** presolve cache */ - NodeSet d_presolve_in; - NodeList d_presolve_cache; - BoolList d_presolve_cache_wq; - BoolList d_presolve_cache_wic; public: QuantifiersEngine(context::Context* c, context::UserContext* u, TheoryEngine* te); ~QuantifiersEngine(); + //---------------------- external interface /** get theory engine */ - TheoryEngine* getTheoryEngine() { return d_te; } - /** get equality query */ - EqualityQuery* getEqualityQuery(); - /** get the equality inference */ - quantifiers::EqualityInference* getEqualityInference() { return d_eq_inference; } + TheoryEngine* getTheoryEngine() const { return d_te; } /** get default sat context for quantifiers engine */ context::Context* getSatContext(); /** get default sat context for quantifiers engine */ @@ -222,42 +105,56 @@ public: Valuation& getValuation(); /** get the logic info for the quantifiers engine */ const LogicInfo& getLogicInfo() const; + //---------------------- end external interface + //---------------------- utilities + /** get equality query */ + EqualityQuery* getEqualityQuery() const; + /** get the equality inference */ + quantifiers::EqualityInference* getEqualityInference() const; /** get relevant domain */ - quantifiers::RelevantDomain* getRelevantDomain() { return d_rel_dom; } + quantifiers::RelevantDomain* getRelevantDomain() const; /** get the BV inverter utility */ - quantifiers::BvInverter * getBvInverter() { return d_bv_invert; } + quantifiers::BvInverter* getBvInverter() const; /** get quantifier relevance */ - quantifiers::QuantRelevance* getQuantifierRelevance() { return d_quant_rel; } + quantifiers::QuantRelevance* getQuantifierRelevance() const; /** get the model builder */ - quantifiers::QModelBuilder* getModelBuilder() { return d_builder; } + quantifiers::QModelBuilder* getModelBuilder() const; /** get utility for EPR */ - quantifiers::QuantEPR* getQuantEPR() { return d_qepr; } - public: // modules - /** get instantiation engine */ - quantifiers::InstantiationEngine* getInstantiationEngine() { return d_inst_engine; } - /** get model engine */ - quantifiers::ModelEngine* getModelEngine() { return d_model_engine; } + quantifiers::QuantEPR* getQuantEPR() const; + /** get model */ + quantifiers::FirstOrderModel* getModel() const; + /** get term database */ + quantifiers::TermDb* getTermDatabase() const; + /** get term database sygus */ + quantifiers::TermDbSygus* getTermDatabaseSygus() const; + /** get term utilities */ + quantifiers::TermUtil* getTermUtil() const; + /** get quantifiers attributes */ + quantifiers::QuantAttributes* getQuantAttributes() const; + /** get instantiate utility */ + quantifiers::Instantiate* getInstantiate() const; + /** get skolemize utility */ + quantifiers::Skolemize* getSkolemize() const; + /** get term enumeration utility */ + quantifiers::TermEnumeration* getTermEnumeration() const; + /** get trigger database */ + inst::TriggerTrie* getTriggerDatabase() const; + //---------------------- end utilities + //---------------------- modules /** get bounded integers utility */ - quantifiers::BoundedIntegers * getBoundedIntegers() { return d_bint; } + quantifiers::BoundedIntegers* getBoundedIntegers() const; /** Conflict find mechanism for quantifiers */ - quantifiers::QuantConflictFind* getConflictFind() { return d_qcf; } + quantifiers::QuantConflictFind* getConflictFind() const; /** rewrite rules utility */ - quantifiers::RewriteEngine * getRewriteEngine() { return d_rr_engine; } - /** subgoal generator */ - quantifiers::ConjectureGenerator * getConjectureGenerator() { return d_sg_gen; } + quantifiers::RewriteEngine* getRewriteEngine() const; /** ceg instantiation */ - quantifiers::CegInstantiation * getCegInstantiation() { return d_ceg_inst; } - /** local theory ext partial inst */ - quantifiers::LtePartialInst * getLtePartialInst() { return d_lte_part_inst; } + quantifiers::CegInstantiation* getCegInstantiation() const; /** get full saturation */ - quantifiers::InstStrategyEnum* getInstStrategyEnum() { return d_fs; } + quantifiers::InstStrategyEnum* getInstStrategyEnum() const; /** get inst strategy cbqi */ - quantifiers::InstStrategyCbqi * getInstStrategyCbqi() { return d_i_cbqi; } - /** get quantifiers splitting */ - quantifiers::QuantDSplit * getQuantDSplit() { return d_qsplit; } - /** get quantifiers anti-skolemization */ - quantifiers::QuantAntiSkolem * getQuantAntiSkolem() { return d_anti_skolem; } -private: + quantifiers::InstStrategyCbqi* getInstStrategyCbqi() const; + //---------------------- end modules + private: /** owner of quantified formulas */ std::map< Node, QuantifiersModule * > d_owner; std::map< Node, int > d_owner_priority; @@ -331,29 +228,6 @@ public: /** get user pat mode */ quantifiers::UserPatMode getInstUserPatMode(); public: - /** get model */ - quantifiers::FirstOrderModel* getModel() { return d_model; } - /** get term database */ - quantifiers::TermDb* getTermDatabase() { return d_term_db; } - /** get term database sygus */ - quantifiers::TermDbSygus * getTermDatabaseSygus() { return d_sygus_tdb; } - /** get term utilities */ - quantifiers::TermUtil* getTermUtil() { return d_term_util; } - /** get quantifiers attributes */ - quantifiers::QuantAttributes* getQuantAttributes() { - return d_quant_attr.get(); - } - /** get instantiate utility */ - quantifiers::Instantiate* getInstantiate() { return d_instantiate.get(); } - /** get skolemize utility */ - quantifiers::Skolemize* getSkolemize() { return d_skolemize.get(); } - /** get term enumeration utility */ - quantifiers::TermEnumeration* getTermEnumeration() - { - return d_term_enum.get(); - } - /** get trigger database */ - inst::TriggerTrie* getTriggerDatabase() { return d_tr_trie; } /** add term to database */ void addTermToDatabase( Node n, bool withinQuant = false, bool withinInstClosure = false ); /** notification when master equality engine is updated */ @@ -439,6 +313,117 @@ public: ~Statistics(); };/* class QuantifiersEngine::Statistics */ Statistics d_statistics; + + private: + /** reference to theory engine object */ + TheoryEngine* d_te; + /** vector of utilities for quantifiers */ + std::vector<QuantifiersUtil*> d_util; + /** vector of modules for quantifiers */ + std::vector<QuantifiersModule*> d_modules; + //------------- quantifiers utilities + /** equality query class */ + std::unique_ptr<quantifiers::EqualityQueryQuantifiersEngine> d_eq_query; + /** equality inference class */ + std::unique_ptr<quantifiers::EqualityInference> d_eq_inference; + /** quantifiers instantiation propagtor */ + std::unique_ptr<quantifiers::InstPropagator> d_inst_prop; + /** all triggers will be stored in this trie */ + std::unique_ptr<inst::TriggerTrie> d_tr_trie; + /** extended model object */ + std::unique_ptr<quantifiers::FirstOrderModel> d_model; + /** for computing relevance of quantifiers */ + std::unique_ptr<quantifiers::QuantRelevance> d_quant_rel; + /** relevant domain */ + std::unique_ptr<quantifiers::RelevantDomain> d_rel_dom; + /** inversion utility for BV instantiation */ + std::unique_ptr<quantifiers::BvInverter> d_bv_invert; + /** model builder */ + std::unique_ptr<quantifiers::QModelBuilder> d_builder; + /** utility for effectively propositional logic */ + std::unique_ptr<quantifiers::QuantEPR> d_qepr; + /** term utilities */ + std::unique_ptr<quantifiers::TermUtil> d_term_util; + /** term database */ + std::unique_ptr<quantifiers::TermDb> d_term_db; + /** sygus term database */ + std::unique_ptr<quantifiers::TermDbSygus> d_sygus_tdb; + /** quantifiers attributes */ + std::unique_ptr<quantifiers::QuantAttributes> d_quant_attr; + /** instantiate utility */ + std::unique_ptr<quantifiers::Instantiate> d_instantiate; + /** skolemize utility */ + std::unique_ptr<quantifiers::Skolemize> d_skolemize; + /** term enumeration utility */ + std::unique_ptr<quantifiers::TermEnumeration> d_term_enum; + //------------- end quantifiers utilities + //------------- quantifiers modules + /** alpha equivalence */ + std::unique_ptr<quantifiers::AlphaEquivalence> d_alpha_equiv; + /** instantiation engine */ + std::unique_ptr<quantifiers::InstantiationEngine> d_inst_engine; + /** model engine */ + std::unique_ptr<quantifiers::ModelEngine> d_model_engine; + /** bounded integers utility */ + std::unique_ptr<quantifiers::BoundedIntegers> d_bint; + /** Conflict find mechanism for quantifiers */ + std::unique_ptr<quantifiers::QuantConflictFind> d_qcf; + /** rewrite rules utility */ + std::unique_ptr<quantifiers::RewriteEngine> d_rr_engine; + /** subgoal generator */ + std::unique_ptr<quantifiers::ConjectureGenerator> d_sg_gen; + /** ceg instantiation */ + std::unique_ptr<quantifiers::CegInstantiation> d_ceg_inst; + /** lte partial instantiation */ + std::unique_ptr<quantifiers::LtePartialInst> d_lte_part_inst; + /** full saturation */ + std::unique_ptr<quantifiers::InstStrategyEnum> d_fs; + /** counterexample-based quantifier instantiation */ + std::unique_ptr<quantifiers::InstStrategyCbqi> d_i_cbqi; + /** quantifiers splitting */ + std::unique_ptr<quantifiers::QuantDSplit> d_qsplit; + /** quantifiers anti-skolemization */ + std::unique_ptr<quantifiers::QuantAntiSkolem> d_anti_skolem; + //------------- end quantifiers modules + //------------- temporary information during check + /** current effort level */ + QuantifiersModule::QEffort d_curr_effort_level; + /** are we in conflict */ + bool d_conflict; + context::CDO<bool> d_conflict_c; + /** has added lemma this round */ + bool d_hasAddedLemma; + /** whether to use model equality engine */ + bool d_useModelEe; + //------------- end temporary information during check + private: + /** list of all quantifiers seen */ + std::map<Node, bool> d_quants; + /** quantifiers pre-registered */ + NodeSet d_quants_prereg; + /** quantifiers reduced */ + BoolMap d_quants_red; + std::map<Node, Node> d_quants_red_lem; + /** list of all lemmas produced */ + // std::map< Node, bool > d_lemmas_produced; + BoolMap d_lemmas_produced_c; + /** lemmas waiting */ + std::vector<Node> d_lemmas_waiting; + /** phase requirements waiting */ + std::map<Node, bool> d_phase_req_waiting; + /** inst round counters TODO: make context-dependent? */ + context::CDO<int> d_ierCounter_c; + int d_ierCounter; + int d_ierCounter_lc; + int d_ierCounterLastLc; + int d_inst_when_phase; + /** has presolve been called */ + context::CDO<bool> d_presolve; + /** presolve cache */ + NodeSet d_presolve_in; + NodeList d_presolve_cache; + BoolList d_presolve_cache_wq; + BoolList d_presolve_cache_wic; };/* class QuantifiersEngine */ }/* CVC4::theory namespace */ diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index ab9fa6d54..317080ba6 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -37,25 +37,28 @@ namespace sets { TheorySetsPrivate::TheorySetsPrivate(TheorySets& external, context::Context* c, - context::UserContext* u): - d_rels(NULL), - d_members(c), - d_deq(c), - d_deq_processed(u), - d_keep(c), - d_proxy(u), - d_proxy_to_term(u), - d_lemmas_produced(u), - d_card_processed(u), - d_var_elim(u), - d_external(external), - d_notify(*this), - d_equalityEngine(d_notify, c, "theory::sets::ee", true), - d_conflict(c) + context::UserContext* u) + : d_members(c), + d_deq(c), + d_deq_processed(u), + d_keep(c), + d_sentLemma(false), + d_addedFact(false), + d_full_check_incomplete(false), + d_proxy(u), + d_proxy_to_term(u), + d_lemmas_produced(u), + d_card_enabled(false), + d_card_processed(u), + d_var_elim(u), + d_external(external), + d_notify(*this), + d_equalityEngine(d_notify, c, "theory::sets::ee", true), + d_conflict(c), + d_rels( + new TheorySetsRels(c, u, &d_equalityEngine, &d_conflict, external)), + d_rels_enabled(false) { - - d_rels = new TheorySetsRels(c, u, &d_equalityEngine, &d_conflict, external); - d_true = NodeManager::currentNM()->mkConst( true ); d_false = NodeManager::currentNM()->mkConst( false ); d_zero = NodeManager::currentNM()->mkConst( Rational(0) ); @@ -68,21 +71,14 @@ TheorySetsPrivate::TheorySetsPrivate(TheorySets& external, d_equalityEngine.addFunctionKind(kind::MEMBER); d_equalityEngine.addFunctionKind(kind::SUBSET); - // If cardinality is on. d_equalityEngine.addFunctionKind(kind::CARD); - - d_card_enabled = false; - d_rels_enabled = false; - -}/* TheorySetsPrivate::TheorySetsPrivate() */ +} TheorySetsPrivate::~TheorySetsPrivate(){ - delete d_rels; for (std::pair<const Node, EqcInfo*>& current_pair : d_eqc_info) { delete current_pair.second; } -}/* TheorySetsPrivate::~TheorySetsPrivate() */ - +} void TheorySetsPrivate::eqNotifyNewClass(TNode t) { if( t.getKind()==kind::SINGLETON || t.getKind()==kind::EMPTYSET ){ diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h index 31aec85c3..d36e0ddb1 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -46,8 +46,6 @@ class TheorySetsPrivate { typedef context::CDHashMap< Node, int, NodeHashFunction> NodeIntMap; typedef context::CDHashSet<Node, NodeHashFunction> NodeSet; typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap; -private: - TheorySetsRels * d_rels; public: void eqNotifyNewClass(TNode t); void eqNotifyPreMerge(TNode t1, TNode t2); @@ -113,9 +111,25 @@ private: void addEqualityToExp( Node a, Node b, std::vector< Node >& exp ); void debugPrintSet( Node s, const char * c ); - + + /** sent lemma + * + * This flag is set to true during a full effort check if this theory + * called d_out->lemma(...). + */ bool d_sentLemma; + /** added fact + * + * This flag is set to true during a full effort check if this theory + * added an internal fact to its equality engine. + */ bool d_addedFact; + /** full check incomplete + * + * This flag is set to true during a full effort check if this theory + * is incomplete for some reason (for instance, if we combine cardinality + * with a relation or extended function kind). + */ bool d_full_check_incomplete; NodeMap d_proxy; NodeMap d_proxy_to_term; @@ -139,11 +153,15 @@ private: std::map< Kind, std::map< Node, std::map< Node, Node > > > d_bop_index; std::map< Kind, std::vector< Node > > d_op_list; //cardinality -private: + private: + /** is cardinality enabled? + * + * This flag is set to true during a full effort check if any constraint + * involving cardinality constraints is asserted to this theory. + */ bool d_card_enabled; /** element types of sets for which cardinality is enabled */ std::map<TypeNode, bool> d_t_card_enabled; - bool d_rels_enabled; std::map< Node, Node > d_eqc_to_card_term; NodeSet d_card_processed; std::map< Node, std::vector< Node > > d_card_parent; @@ -300,7 +318,16 @@ private: bool isCareArg( Node n, unsigned a ); public: bool isEntailed( Node n, bool pol ); - + + private: + /** subtheory solver for the theory of relations */ + std::unique_ptr<TheorySetsRels> d_rels; + /** are relations enabled? + * + * This flag is set to true during a full effort check if any constraint + * involving relational constraints is asserted to this theory. + */ + bool d_rels_enabled; };/* class TheorySetsPrivate */ diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index 477e99b9b..f53f82cc4 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -34,7 +34,6 @@ RegExpOpr::RegExpOpr() std::vector<Node>{})), d_zero(NodeManager::currentNM()->mkConst(::CVC4::Rational(0))), d_one(NodeManager::currentNM()->mkConst(::CVC4::Rational(1))), - RMAXINT(LONG_MAX), d_sigma(NodeManager::currentNM()->mkNode(kind::REGEXP_SIGMA, std::vector<Node>{})), d_sigma_star(NodeManager::currentNM()->mkNode(kind::REGEXP_STAR, d_sigma)) @@ -1137,7 +1136,8 @@ bool RegExpOpr::isPairNodesInSet(std::set< PairNodes > &s, Node n1, Node n2) { bool RegExpOpr::containC2(unsigned cnt, Node n) { if(n.getKind() == kind::REGEXP_RV) { - Assert(n[0].getConst<Rational>() <= RMAXINT, "Exceeded LONG_MAX in RegExpOpr::containC2"); + Assert(n[0].getConst<Rational>() <= Rational(String::maxSize()), + "Exceeded UINT32_MAX in RegExpOpr::containC2"); unsigned y = n[0].getConst<Rational>().getNumerator().toUnsignedInt(); return cnt == y; } else if(n.getKind() == kind::REGEXP_CONCAT) { @@ -1178,7 +1178,8 @@ void RegExpOpr::convert2(unsigned cnt, Node n, Node &r1, Node &r2) { r1 = d_emptySingleton; r2 = d_emptySingleton; } else if(n.getKind() == kind::REGEXP_RV) { - Assert(n[0].getConst<Rational>() <= RMAXINT, "Exceeded LONG_MAX in RegExpOpr::convert2"); + Assert(n[0].getConst<Rational>() <= Rational(String::maxSize()), + "Exceeded UINT32_MAX in RegExpOpr::convert2"); unsigned y = n[0].getConst<Rational>().getNumerator().toUnsignedInt(); r1 = d_emptySingleton; if(cnt == y) { diff --git a/src/theory/strings/regexp_operation.h b/src/theory/strings/regexp_operation.h index a646f0e6f..57e68abfb 100644 --- a/src/theory/strings/regexp_operation.h +++ b/src/theory/strings/regexp_operation.h @@ -48,7 +48,6 @@ class RegExpOpr { Node d_emptyRegexp; Node d_zero; Node d_one; - CVC4::Rational RMAXINT; Node d_sigma; Node d_sigma_star; diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index ce0100686..72e82edca 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -103,7 +103,6 @@ TheoryStrings::TheoryStrings(context::Context* c, Valuation valuation, const LogicInfo& logicInfo) : Theory(THEORY_STRINGS, c, u, out, valuation, logicInfo), - RMAXINT(LONG_MAX), d_notify(*this), d_equalityEngine(d_notify, c, "theory::strings", true), d_conflict(c, false), @@ -536,7 +535,8 @@ bool TheoryStrings::collectModelInfo(TheoryModel* m) Trace("strings-model") << " } (length is " << lts[i] << ")" << std::endl; if( lts[i].isConst() ) { lts_values.push_back( lts[i] ); - Assert(lts[i].getConst<Rational>() <= RMAXINT, "Exceeded LONG_MAX in string model"); + Assert(lts[i].getConst<Rational>() <= Rational(String::maxSize()), + "Exceeded UINT32_MAX in string model"); unsigned lvalue = lts[i].getConst<Rational>().getNumerator().toUnsignedInt(); values_used[ lvalue ] = true; }else{ @@ -545,7 +545,8 @@ bool TheoryStrings::collectModelInfo(TheoryModel* m) Node v = d_valuation.getModelValue(lts[i]); Trace("strings-model") << "Model value for " << lts[i] << " is " << v << std::endl; lts_values.push_back( v ); - Assert(v.getConst<Rational>() <= RMAXINT, "Exceeded LONG_MAX in string model"); + Assert(v.getConst<Rational>() <= Rational(String::maxSize()), + "Exceeded UINT32_MAX in string model"); unsigned lvalue = v.getConst<Rational>().getNumerator().toUnsignedInt(); values_used[ lvalue ] = true; }else{ @@ -621,7 +622,8 @@ bool TheoryStrings::collectModelInfo(TheoryModel* m) Trace("strings-model") << std::endl; //use type enumerator - Assert(lts_values[i].getConst<Rational>() <= RMAXINT, "Exceeded LONG_MAX in string model"); + Assert(lts_values[i].getConst<Rational>() <= Rational(String::maxSize()), + "Exceeded UINT32_MAX in string model"); StringEnumeratorLength sel(lts_values[i].getConst<Rational>().getNumerator().toUnsignedInt()); for (const Node& eqc : pure_eq) { diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index de505f262..2c0cb42aa 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -234,7 +234,6 @@ private: Node d_zero; Node d_one; Node d_neg_one; - CVC4::Rational RMAXINT; unsigned d_card_size; // Helper functions Node getRepresentative( Node t ); diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index 9a0fad7d8..1c68097ae 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -653,13 +653,13 @@ Node TheoryStringsRewriter::rewriteLoopRegExp(TNode node) } TNode n1 = node[1]; NodeManager* nm = NodeManager::currentNM(); - CVC4::Rational RMAXINT(LONG_MAX); + CVC4::Rational rMaxInt(String::maxSize()); AlwaysAssert(n1.isConst(), "re.loop contains non-constant integer (1)."); AlwaysAssert(n1.getConst<Rational>().sgn() >= 0, "Negative integer in string REGEXP_LOOP (1)"); - Assert(n1.getConst<Rational>() <= RMAXINT, - "Exceeded LONG_MAX in string REGEXP_LOOP (1)"); - unsigned l = n1.getConst<Rational>().getNumerator().toUnsignedInt(); + Assert(n1.getConst<Rational>() <= rMaxInt, + "Exceeded UINT32_MAX in string REGEXP_LOOP (1)"); + uint32_t l = n1.getConst<Rational>().getNumerator().toUnsignedInt(); std::vector<Node> vec_nodes; for (unsigned i = 0; i < l; i++) { @@ -675,9 +675,9 @@ Node TheoryStringsRewriter::rewriteLoopRegExp(TNode node) AlwaysAssert(n2.isConst(), "re.loop contains non-constant integer (2)."); AlwaysAssert(n2.getConst<Rational>().sgn() >= 0, "Negative integer in string REGEXP_LOOP (2)"); - Assert(n2.getConst<Rational>() <= RMAXINT, - "Exceeded LONG_MAX in string REGEXP_LOOP (2)"); - unsigned u = n2.getConst<Rational>().getNumerator().toUnsignedInt(); + Assert(n2.getConst<Rational>() <= rMaxInt, + "Exceeded UINT32_MAX in string REGEXP_LOOP (2)"); + uint32_t u = n2.getConst<Rational>().getNumerator().toUnsignedInt(); if (u <= l) { retNode = n; @@ -838,7 +838,7 @@ bool TheoryStringsRewriter::testConstStringInRegExp( CVC4::String &s, unsigned i } } case kind::REGEXP_LOOP: { - unsigned l = r[1].getConst<Rational>().getNumerator().toUnsignedInt(); + uint32_t l = r[1].getConst<Rational>().getNumerator().toUnsignedInt(); if(s.size() == index_start) { return l==0? true : testConstStringInRegExp(s, index_start, r[0]); } else if(l==0 && r[1]==r[2]) { @@ -847,7 +847,7 @@ bool TheoryStringsRewriter::testConstStringInRegExp( CVC4::String &s, unsigned i Assert(r.getNumChildren() == 3, "String rewriter error: LOOP has 2 children"); if(l==0) { //R{0,u} - unsigned u = r[2].getConst<Rational>().getNumerator().toUnsignedInt(); + uint32_t u = r[2].getConst<Rational>().getNumerator().toUnsignedInt(); for(unsigned len=s.size() - index_start; len>=1; len--) { CVC4::String t = s.substr(index_start, len); if(testConstStringInRegExp(t, 0, r[0])) { @@ -1216,9 +1216,9 @@ Node TheoryStringsRewriter::rewriteSubstr(Node node) if (node[1].isConst() && node[2].isConst()) { CVC4::String s = node[0].getConst<String>(); - CVC4::Rational RMAXINT(LONG_MAX); - unsigned start; - if (node[1].getConst<Rational>() > RMAXINT) + CVC4::Rational rMaxInt(String::maxSize()); + uint32_t start; + if (node[1].getConst<Rational>() > rMaxInt) { // start beyond the maximum size of strings // thus, it must be beyond the end point of this string @@ -1241,7 +1241,7 @@ Node TheoryStringsRewriter::rewriteSubstr(Node node) return returnRewrite(node, ret, "ss-const-start-oob"); } } - if (node[2].getConst<Rational>() > RMAXINT) + if (node[2].getConst<Rational>() > rMaxInt) { // take up to the end of the string Node ret = nm->mkConst(::CVC4::String(s.suffix(s.size() - start))); @@ -1254,7 +1254,7 @@ Node TheoryStringsRewriter::rewriteSubstr(Node node) } else { - unsigned len = + uint32_t len = node[2].getConst<Rational>().getNumerator().toUnsignedInt(); if (start + len > s.size()) { @@ -1743,17 +1743,17 @@ Node TheoryStringsRewriter::rewriteIndexof( Node node ) { getConcat(node[0], children0); if (children0[0].isConst() && node[1].isConst() && node[2].isConst()) { - CVC4::Rational RMAXINT(CVC4::String::maxSize()); - if (node[2].getConst<Rational>() > RMAXINT) + CVC4::Rational rMaxInt(CVC4::String::maxSize()); + if (node[2].getConst<Rational>() > rMaxInt) { // We know that, due to limitations on the size of string constants // in our implementation, that accessing a position greater than - // RMAXINT is guaranteed to be out of bounds. + // rMaxInt is guaranteed to be out of bounds. Node negone = nm->mkConst(Rational(-1)); return returnRewrite(node, negone, "idof-max"); } Assert(node[2].getConst<Rational>().sgn() >= 0); - unsigned start = + uint32_t start = node[2].getConst<Rational>().getNumerator().toUnsignedInt(); CVC4::String s = children0[0].getConst<String>(); CVC4::String t = node[1].getConst<String>(); @@ -2641,10 +2641,10 @@ bool TheoryStringsRewriter::stripSymbolicLength(std::vector<Node>& n1, // we can remove part of the constant // lower bound minus the length of a concrete string is negative, // hence lowerBound cannot be larger than long max - Assert(lbr < Rational(LONG_MAX)); + Assert(lbr < Rational(String::maxSize())); curr = Rewriter::rewrite(NodeManager::currentNM()->mkNode( kind::MINUS, curr, lowerBound)); - unsigned lbsize = lbr.getNumerator().toUnsignedInt(); + uint32_t lbsize = lbr.getNumerator().toUnsignedInt(); Assert(lbsize < s.size()); if (dir == 1) { diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index c87a4be02..d75f7843d 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -49,7 +49,6 @@ #include "theory/theory_model.h" #include "theory/theory_traits.h" #include "theory/uf/equality_engine.h" -#include "theory/unconstrained_simplifier.h" #include "util/resource_manager.h" using namespace std; @@ -315,7 +314,6 @@ TheoryEngine::TheoryEngine(context::Context* context, d_factsAsserted(context, false), d_preRegistrationVisitor(this, context), d_sharedTermsVisitor(d_sharedTerms), - d_unconstrainedSimp(new UnconstrainedSimplifier(context, logicInfo)), d_theoryAlternatives(), d_attr_handle(), d_arithSubstitutionsAdded("theory::arith::zzz::arith::substitutions", 0) @@ -360,9 +358,6 @@ TheoryEngine::~TheoryEngine() { delete d_masterEqualityEngine; smtStatisticsRegistry()->unregisterStat(&d_combineTheoriesTime); - - delete d_unconstrainedSimp; - smtStatisticsRegistry()->unregisterStat(&d_arithSubstitutionsAdded); } @@ -2146,11 +2141,6 @@ void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector }); } -void TheoryEngine::ppUnconstrainedSimp(vector<Node>& assertions) -{ - d_unconstrainedSimp->processAssertions(assertions); -} - void TheoryEngine::setUserAttribute(const std::string& attr, Node n, const std::vector<Node>& node_values, diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 71a0234ed..65402f0a6 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -99,7 +99,6 @@ namespace theory { class DecisionEngine; class RemoveTermFormulas; -class UnconstrainedSimplifier; /** * This is essentially an abstraction for a collection of theories. A @@ -827,9 +826,6 @@ private: /** Dump the assertions to the dump */ void dumpAssertions(const char* tag); - /** For preprocessing pass simplifying unconstrained expressions */ - UnconstrainedSimplifier* d_unconstrainedSimp; - /** For preprocessing pass lifting bit-vectors of size 1 to booleans */ public: void staticInitializeBVOptions(const std::vector<Node>& assertions); @@ -838,8 +834,6 @@ public: /** Returns false if an assertion simplified to false. */ bool donePPSimpITE(std::vector<Node>& assertions); - void ppUnconstrainedSimp(std::vector<Node>& assertions); - SharedTermsDatabase* getSharedTermsDatabase() { return &d_sharedTerms; } theory::eq::EqualityEngine* getMasterEqualityEngine() { return d_masterEqualityEngine; } diff --git a/src/theory/unconstrained_simplifier.cpp b/src/theory/unconstrained_simplifier.cpp deleted file mode 100644 index 41529760b..000000000 --- a/src/theory/unconstrained_simplifier.cpp +++ /dev/null @@ -1,704 +0,0 @@ -/********************* */ -/*! \file unconstrained_simplifier.cpp - ** \verbatim - ** Top contributors (to current version): - ** Clark Barrett, Tim King, Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 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 Simplifications based on unconstrained variables - ** - ** This module implements a preprocessing phase which replaces certain "unconstrained" expressions - ** by variables. Based on Roberto Bruttomesso's PhD thesis. - **/ - - -#include "theory/unconstrained_simplifier.h" - -#include "theory/rewriter.h" -#include "theory/logic_info.h" -#include "smt/smt_statistics_registry.h" - -using namespace std; -using namespace CVC4; -using namespace theory; - - -UnconstrainedSimplifier::UnconstrainedSimplifier(context::Context* context, - const LogicInfo& logicInfo) - : d_numUnconstrainedElim("preprocessor::number of unconstrained elims", 0), - d_context(context), d_substitutions(context), d_logicInfo(logicInfo) -{ - smtStatisticsRegistry()->registerStat(&d_numUnconstrainedElim); -} - - -UnconstrainedSimplifier::~UnconstrainedSimplifier() -{ - smtStatisticsRegistry()->unregisterStat(&d_numUnconstrainedElim); -} - - -struct unc_preprocess_stack_element { - TNode node; - TNode parent; - unc_preprocess_stack_element(TNode n) : node(n) {} - unc_preprocess_stack_element(TNode n, TNode p) : node(n), parent(p) {} -};/* struct unc_preprocess_stack_element */ - - -void UnconstrainedSimplifier::visitAll(TNode assertion) -{ - // Do a topological sort of the subexpressions and substitute them - vector<unc_preprocess_stack_element> toVisit; - toVisit.push_back(assertion); - - while (!toVisit.empty()) - { - // The current node we are processing - TNode current = toVisit.back().node; - TNode parent = toVisit.back().parent; - toVisit.pop_back(); - - TNodeCountMap::iterator find = d_visited.find(current); - if (find != d_visited.end()) { - if (find->second == 1) { - d_visitedOnce.erase(current); - if (current.isVar()) { - d_unconstrained.erase(current); - } - } - ++find->second; - continue; - } - - d_visited[current] = 1; - d_visitedOnce[current] = parent; - - if (current.getNumChildren() == 0) { - if (current.getKind()==kind::VARIABLE || current.getKind()==kind::SKOLEM) { - d_unconstrained.insert(current); - } - } - else { - for(TNode::iterator child_it = current.begin(); child_it != current.end(); ++ child_it) { - TNode childNode = *child_it; - toVisit.push_back(unc_preprocess_stack_element(childNode, current)); - } - } - } -} - -Node UnconstrainedSimplifier::newUnconstrainedVar(TypeNode t, TNode var) -{ - Node n = NodeManager::currentNM()->mkSkolem("unconstrained", t, "a new var introduced because of unconstrained variable " + var.toString()); - return n; -} - - -void UnconstrainedSimplifier::processUnconstrained() -{ - TNodeSet::iterator it = d_unconstrained.begin(), iend = d_unconstrained.end(); - vector<TNode> workList; - for ( ; it != iend; ++it) { - workList.push_back(*it); - } - Node currentSub; - TNode parent; - bool swap; - bool isSigned; - bool strict; - vector<TNode> delayQueueLeft; - vector<Node> delayQueueRight; - - TNode current = workList.back(); - workList.pop_back(); - for (;;) { - Assert(d_visitedOnce.find(current) != d_visitedOnce.end()); - parent = d_visitedOnce[current]; - if (!parent.isNull()) { - swap = isSigned = strict = false; - bool checkParent = false; - switch (parent.getKind()) { - - // If-then-else operator - any two unconstrained children makes the parent unconstrained - case kind::ITE: { - Assert(parent[0] == current || parent[1] == current || parent[2] == current); - bool uCond = parent[0] == current || d_unconstrained.find(parent[0]) != d_unconstrained.end(); - bool uThen = parent[1] == current || d_unconstrained.find(parent[1]) != d_unconstrained.end(); - bool uElse = parent[2] == current || d_unconstrained.find(parent[2]) != d_unconstrained.end(); - if ((uCond && uThen) || (uCond && uElse) || (uThen && uElse)) { - if (d_unconstrained.find(parent) == d_unconstrained.end() && - !d_substitutions.hasSubstitution(parent)) { - ++d_numUnconstrainedElim; - if (uThen) { - if (parent[1] != current) { - if (parent[1].isVar()) { - currentSub = parent[1]; - } - else { - Assert(d_substitutions.hasSubstitution(parent[1])); - currentSub = d_substitutions.apply(parent[1]); - } - } - else if (currentSub.isNull()) { - currentSub = current; - } - } - else if (parent[2] != current) { - if (parent[2].isVar()) { - currentSub = parent[2]; - } - else { - Assert(d_substitutions.hasSubstitution(parent[2])); - currentSub = d_substitutions.apply(parent[2]); - } - } - else if (currentSub.isNull()) { - currentSub = current; - } - current = parent; - } - else { - currentSub = Node(); - } - } - else if (uCond) { - Cardinality card = parent.getType().getCardinality(); - if (card.isFinite() && !card.isLargeFinite() && card.getFiniteCardinality() == 2) { - // Special case: condition is unconstrained, then and else are different, and total cardinality of the type is 2, then the result - // is unconstrained - Node test = Rewriter::rewrite(parent[1].eqNode(parent[2])); - if (test == NodeManager::currentNM()->mkConst<bool>(false)) { - ++d_numUnconstrainedElim; - if (currentSub.isNull()) { - currentSub = current; - } - currentSub = newUnconstrainedVar(parent.getType(), currentSub); - current = parent; - } - } - } - break; - } - - // Comparisons that return a different type - assuming domains are larger than 1, any - // unconstrained child makes parent unconstrained as well - case kind::EQUAL: - if (parent[0].getType() != parent[1].getType()) { - TNode other = (parent[0] == current) ? parent[1] : parent[0]; - if (current.getType().isSubtypeOf(other.getType())) { - break; - } - } - if( parent[0].getType().isDatatype() ){ - TypeNode tn = parent[0].getType(); - const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); - if( dt.isRecursiveSingleton( tn.toType() ) ){ - //domain size may be 1 - break; - } - } - if( parent[0].getType().isBoolean() ){ - checkParent = true; - break; - } - case kind::BITVECTOR_COMP: - case kind::LT: - case kind::LEQ: - case kind::GT: - case kind::GEQ: - { - if (d_unconstrained.find(parent) == d_unconstrained.end() && - !d_substitutions.hasSubstitution(parent)) { - ++d_numUnconstrainedElim; - Assert(parent[0] != parent[1] && - (parent[0] == current || parent[1] == current)); - if (currentSub.isNull()) { - currentSub = current; - } - currentSub = newUnconstrainedVar(parent.getType(), currentSub); - current = parent; - } - else { - currentSub = Node(); - } - break; - } - - // Unary operators that propagate unconstrainedness - case kind::NOT: - case kind::BITVECTOR_NOT: - case kind::BITVECTOR_NEG: - case kind::UMINUS: - ++d_numUnconstrainedElim; - Assert(parent[0] == current); - if (currentSub.isNull()) { - currentSub = current; - } - current = parent; - break; - - // Unary operators that propagate unconstrainedness and return a different type - case kind::BITVECTOR_EXTRACT: - ++d_numUnconstrainedElim; - Assert(parent[0] == current); - if (currentSub.isNull()) { - currentSub = current; - } - currentSub = newUnconstrainedVar(parent.getType(), currentSub); - current = parent; - break; - - // Operators returning same type requiring all children to be unconstrained - case kind::AND: - case kind::OR: - case kind::IMPLIES: - case kind::BITVECTOR_AND: - case kind::BITVECTOR_OR: - case kind::BITVECTOR_NAND: - case kind::BITVECTOR_NOR: - { - bool allUnconstrained = true; - for(TNode::iterator child_it = parent.begin(); child_it != parent.end(); ++child_it) { - if (d_unconstrained.find(*child_it) == d_unconstrained.end()) { - allUnconstrained = false; - break; - } - } - if (allUnconstrained) { - checkParent = true; - } - } - break; - - // Require all children to be unconstrained and different - case kind::BITVECTOR_SHL: - case kind::BITVECTOR_LSHR: - case kind::BITVECTOR_ASHR: - case kind::BITVECTOR_UDIV_TOTAL: - case kind::BITVECTOR_UREM_TOTAL: - case kind::BITVECTOR_SDIV: - case kind::BITVECTOR_SREM: - case kind::BITVECTOR_SMOD: { - bool allUnconstrained = true; - bool allDifferent = true; - for(TNode::iterator child_it = parent.begin(); child_it != parent.end(); ++child_it) { - if (d_unconstrained.find(*child_it) == d_unconstrained.end()) { - allUnconstrained = false; - break; - } - for(TNode::iterator child_it2 = child_it + 1; child_it2 != parent.end(); ++child_it2) { - if (*child_it == *child_it2) { - allDifferent = false; - break; - } - } - } - if (allUnconstrained && allDifferent) { - checkParent = true; - } - break; - } - - // Requires all children to be unconstrained and different, and returns a different type - case kind::BITVECTOR_CONCAT: - { - bool allUnconstrained = true; - bool allDifferent = true; - for(TNode::iterator child_it = parent.begin(); child_it != parent.end(); ++child_it) { - if (d_unconstrained.find(*child_it) == d_unconstrained.end()) { - allUnconstrained = false; - break; - } - for(TNode::iterator child_it2 = child_it + 1; child_it2 != parent.end(); ++child_it2) { - if (*child_it == *child_it2) { - allDifferent = false; - break; - } - } - } - if (allUnconstrained && allDifferent) { - if (d_unconstrained.find(parent) == d_unconstrained.end() && - !d_substitutions.hasSubstitution(parent)) { - ++d_numUnconstrainedElim; - if (currentSub.isNull()) { - currentSub = current; - } - currentSub = newUnconstrainedVar(parent.getType(), currentSub); - current = parent; - } - else { - currentSub = Node(); - } - } - } - break; - - // N-ary operators returning same type requiring at least one child to be unconstrained - case kind::PLUS: - case kind::MINUS: - if (current.getType().isInteger() && - !parent.getType().isInteger()) { - break; - } - case kind::XOR: - case kind::BITVECTOR_XOR: - case kind::BITVECTOR_XNOR: - case kind::BITVECTOR_PLUS: - case kind::BITVECTOR_SUB: - checkParent = true; - break; - - // Multiplication/division: must be non-integer and other operand must be non-zero - case kind::MULT: { - case kind::DIVISION: - Assert(parent.getNumChildren() == 2); - TNode other; - if (parent[0] == current) { - other = parent[1]; - } - else { - Assert(parent[1] == current); - other = parent[0]; - } - if (d_unconstrained.find(other) != d_unconstrained.end()) { - if (d_unconstrained.find(parent) == d_unconstrained.end() && - !d_substitutions.hasSubstitution(parent)) { - if (current.getType().isInteger() && other.getType().isInteger()) { - Assert(parent.getKind() == kind::DIVISION || parent.getType().isInteger()); - if (parent.getKind() == kind::DIVISION) { - break; - } - } - ++d_numUnconstrainedElim; - if (currentSub.isNull()) { - currentSub = current; - } - current = parent; - } - else { - currentSub = Node(); - } - } - else { - // if only the denominator of a division is unconstrained, can't set it to 0 so the result is not unconstrained - if (parent.getKind() == kind::DIVISION && current == parent[1]) { - break; - } - NodeManager* nm = NodeManager::currentNM(); - // if we are an integer, the only way we are unconstrained is if we are a MULT by -1 - if (current.getType().isInteger()) { - // div/mult by 1 should have been simplified - Assert(other != nm->mkConst<Rational>(1)); - if (other == nm->mkConst<Rational>(-1)) { - // div by -1 should have been simplified - Assert(parent.getKind() == kind::MULT); - Assert(parent.getType().isInteger()); - } - else { - break; - } - } - else { - // TODO: could build ITE here - Node test = other.eqNode(nm->mkConst<Rational>(0)); - if (Rewriter::rewrite(test) != nm->mkConst<bool>(false)) { - break; - } - } - ++d_numUnconstrainedElim; - if (currentSub.isNull()) { - currentSub = current; - } - current = parent; - } - break; - } - - // Bitvector MULT - current must only appear once in the children: - // all other children must be unconstrained or odd - case kind::BITVECTOR_MULT: - { - bool found = false; - bool done = false; - for(TNode::iterator child_it = parent.begin(); child_it != parent.end(); ++child_it) { - if ((*child_it) == current) { - if (found) { - done = true; - break; - } - found = true; - continue; - } - else if (d_unconstrained.find(*child_it) != d_unconstrained.end()) { - continue; - } - else { - NodeManager* nm = NodeManager::currentNM(); - Node extractOp = nm->mkConst<BitVectorExtract>(BitVectorExtract(0,0)); - vector<Node> children; - children.push_back(*child_it); - Node test = nm->mkNode(extractOp, children); - BitVector one(1,unsigned(1)); - test = test.eqNode(nm->mkConst<BitVector>(one)); - if (Rewriter::rewrite(test) != nm->mkConst<bool>(true)) { - done = true; - break; - } - } - } - if (done) { - break; - } - checkParent = true; - break; - } - - // Uninterpreted function - if domain is infinite, no quantifiers are used, and any child is unconstrained, result is unconstrained - case kind::APPLY_UF: - if (d_logicInfo.isQuantified() || !current.getType().getCardinality().isInfinite()) { - break; - } - if (d_unconstrained.find(parent) == d_unconstrained.end() && - !d_substitutions.hasSubstitution(parent)) { - ++d_numUnconstrainedElim; - if (currentSub.isNull()) { - currentSub = current; - } - if (parent.getType() != current.getType()) { - currentSub = newUnconstrainedVar(parent.getType(), currentSub); - } - current = parent; - } - else { - currentSub = Node(); - } - break; - - // Array select - if array is unconstrained, so is result - case kind::SELECT: - if (parent[0] == current) { - ++d_numUnconstrainedElim; - Assert(current.getType().isArray()); - if (currentSub.isNull()) { - currentSub = current; - } - currentSub = newUnconstrainedVar(current.getType().getArrayConstituentType(), currentSub); - current = parent; - } - break; - - // Array store - if both store and value are unconstrained, so is resulting store - case kind::STORE: - if (((parent[0] == current && - d_unconstrained.find(parent[2]) != d_unconstrained.end()) || - (parent[2] == current && - d_unconstrained.find(parent[0]) != d_unconstrained.end()))) { - if (d_unconstrained.find(parent) == d_unconstrained.end() && - !d_substitutions.hasSubstitution(parent)) { - ++d_numUnconstrainedElim; - if (parent[0] != current) { - if (parent[0].isVar()) { - currentSub = parent[0]; - } - else { - Assert(d_substitutions.hasSubstitution(parent[0])); - currentSub = d_substitutions.apply(parent[0]); - } - } - else if (currentSub.isNull()) { - currentSub = current; - } - current = parent; - } - else { - currentSub = Node(); - } - } - break; - - // Bit-vector comparisons: replace with new Boolean variable, but have - // to also conjoin with a side condition as there is always one case - // when the comparison is forced to be false - case kind::BITVECTOR_ULT: - case kind::BITVECTOR_UGE: - case kind::BITVECTOR_UGT: - case kind::BITVECTOR_ULE: - case kind::BITVECTOR_SLT: - case kind::BITVECTOR_SGE: - case kind::BITVECTOR_SGT: - case kind::BITVECTOR_SLE: { - // Tuples over (signed, swap, strict). - switch (parent.getKind()) { - case kind::BITVECTOR_UGE: - break; - case kind::BITVECTOR_ULT: - strict = true; - break; - case kind::BITVECTOR_ULE: - swap = true; - break; - case kind::BITVECTOR_UGT: - swap = true; - strict = true; - break; - case kind::BITVECTOR_SGE: - isSigned = true; - break; - case kind::BITVECTOR_SLT: - isSigned = true; - strict = true; - break; - case kind::BITVECTOR_SLE: - isSigned = true; - swap = true; - break; - case kind::BITVECTOR_SGT: - isSigned = true; - swap = true; - strict = true; - break; - default: - Unreachable(); - } - TNode other; - bool left = false; - if (parent[0] == current) { - other = parent[1]; - left = true; - } else { - Assert(parent[1] == current); - other = parent[0]; - } - if (d_unconstrained.find(other) != d_unconstrained.end()) { - if (d_unconstrained.find(parent) == d_unconstrained.end() && - !d_substitutions.hasSubstitution(parent)) { - ++d_numUnconstrainedElim; - if (currentSub.isNull()) { - currentSub = current; - } - currentSub = newUnconstrainedVar(parent.getType(), currentSub); - current = parent; - } else { - currentSub = Node(); - } - } else { - unsigned size = current.getType().getBitVectorSize(); - BitVector bv = - isSigned ? BitVector(size, Integer(1).multiplyByPow2(size - 1)) - : BitVector(size, unsigned(0)); - if (swap == left) { - bv = ~bv; - } - if (currentSub.isNull()) { - currentSub = current; - } - currentSub = newUnconstrainedVar(parent.getType(), currentSub); - current = parent; - NodeManager* nm = NodeManager::currentNM(); - Node test = - Rewriter::rewrite(other.eqNode(nm->mkConst<BitVector>(bv))); - if (test == nm->mkConst<bool>(false)) { - break; - } - if (strict) { - currentSub = currentSub.andNode(test.notNode()); - } else { - currentSub = currentSub.orNode(test); - } - // Delay adding this substitution - see comment at end of function - delayQueueLeft.push_back(current); - delayQueueRight.push_back(currentSub); - currentSub = Node(); - parent = TNode(); - } - break; - } - - // Do nothing - case kind::BITVECTOR_SIGN_EXTEND: - case kind::BITVECTOR_ZERO_EXTEND: - case kind::BITVECTOR_REPEAT: - case kind::BITVECTOR_ROTATE_LEFT: - case kind::BITVECTOR_ROTATE_RIGHT: - - default: - break; - } - if( checkParent ){ - //run for various cases from above - if (d_unconstrained.find(parent) == d_unconstrained.end() && - !d_substitutions.hasSubstitution(parent)) { - ++d_numUnconstrainedElim; - if (currentSub.isNull()) { - currentSub = current; - } - current = parent; - } - else { - currentSub = Node(); - } - } - if (current == parent && d_visited[parent] == 1) { - d_unconstrained.insert(parent); - continue; - } - } - if (!currentSub.isNull()) { - Assert(currentSub.isVar()); - d_substitutions.addSubstitution(current, currentSub, false); - } - if (workList.empty()) { - break; - } - current = workList.back(); - currentSub = Node(); - workList.pop_back(); - } - TNode left; - Node right; - // All substitutions except those arising from bitvector comparisons are - // substitutions t -> x where x is a variable. This allows us to build the - // substitution very quickly (never invalidating the substitution cache). - // Bitvector comparisons are more complicated and may require - // back-substitution and cache-invalidation. So we do these last. - while (!delayQueueLeft.empty()) { - left = delayQueueLeft.back(); - if (!d_substitutions.hasSubstitution(left)) { - right = d_substitutions.apply(delayQueueRight.back()); - d_substitutions.addSubstitution(delayQueueLeft.back(), right); - } - delayQueueLeft.pop_back(); - delayQueueRight.pop_back(); - } -} - - -void UnconstrainedSimplifier::processAssertions(vector<Node>& assertions) -{ - d_context->push(); - - vector<Node>::iterator it = assertions.begin(), iend = assertions.end(); - for (; it != iend; ++it) { - visitAll(*it); - } - - if (!d_unconstrained.empty()) { - processUnconstrained(); - // d_substitutions.print(Message.getStream()); - for (it = assertions.begin(); it != iend; ++it) { - (*it) = Rewriter::rewrite(d_substitutions.apply(*it)); - } - } - - // to clear substitutions map - d_context->pop(); - - d_visited.clear(); - d_visitedOnce.clear(); - d_unconstrained.clear(); -} diff --git a/src/theory/unconstrained_simplifier.h b/src/theory/unconstrained_simplifier.h deleted file mode 100644 index b13311e2a..000000000 --- a/src/theory/unconstrained_simplifier.h +++ /dev/null @@ -1,67 +0,0 @@ -/********************* */ -/*! \file unconstrained_simplifier.h - ** \verbatim - ** Top contributors (to current version): - ** Clark Barrett, Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 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 Simplifications based on unconstrained variables - ** - ** This module implements a preprocessing phase which replaces certain "unconstrained" expressions - ** by variables. Based on Roberto Bruttomesso's PhD thesis. - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__UNCONSTRAINED_SIMPLIFIER_H -#define __CVC4__UNCONSTRAINED_SIMPLIFIER_H - -#include <unordered_map> -#include <unordered_set> -#include <utility> -#include <vector> - -#include "expr/node.h" -#include "theory/substitutions.h" -#include "util/statistics_registry.h" - -namespace CVC4 { - -/* Forward Declarations */ -class LogicInfo; - -class UnconstrainedSimplifier { - - /** number of expressions eliminated due to unconstrained simplification */ - IntStat d_numUnconstrainedElim; - - typedef std::unordered_map<TNode, unsigned, TNodeHashFunction> TNodeCountMap; - typedef std::unordered_map<TNode, TNode, TNodeHashFunction> TNodeMap; - typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet; - - TNodeCountMap d_visited; - TNodeMap d_visitedOnce; - TNodeSet d_unconstrained; - - context::Context* d_context; - theory::SubstitutionMap d_substitutions; - - const LogicInfo& d_logicInfo; - - void visitAll(TNode assertion); - Node newUnconstrainedVar(TypeNode t, TNode var); - void processUnconstrained(); - -public: - UnconstrainedSimplifier(context::Context* context, const LogicInfo& logicInfo); - ~UnconstrainedSimplifier(); - void processAssertions(std::vector<Node>& assertions); -}; - -} - -#endif |