From: Andrew Reynolds Date: Sun, 27 Jan 2013 17:35:22 +0000 (-0600) Subject: some fixes for Intel benchmarks regarding quantifiers and datatypes, datatypes theory... X-Git-Tag: cvc5-1.0.0~7447 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=bcbf52ffbe0416ecf70bdb644017c338c0540793;p=cvc5.git some fixes for Intel benchmarks regarding quantifiers and datatypes, datatypes theory still crashes for datatypes with boolean subfields --- diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 66c7e4cbc..1d98ce115 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -69,6 +69,7 @@ #include "theory/arrays/options.h" #include "util/sort_inference.h" #include "theory/quantifiers/macros.h" +#include "theory/datatypes/options.h" using namespace std; using namespace CVC4; @@ -977,6 +978,13 @@ void SmtEngine::setLogicInternal() throw() { setOption("check-models", SExpr("false")); } } + + //datatypes theory should assign values to all datatypes terms if logic is quantified + if (d_logic.isQuantified() && d_logic.isTheoryEnabled(theory::THEORY_DATATYPES)) { + if( !options::dtForceAssignment.wasSetByUser() ){ + options::dtForceAssignment.set(true); + } + } } void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value) @@ -2253,7 +2261,7 @@ void SmtEnginePrivate::processAssertions() { collectSkolems((*pos).first, skolemSet, cache); collectSkolems((*pos).second, skolemSet, cache); } - + // We need to ensure: // 1. iteExpr has the form (ite cond (sk = t) (sk = e)) // 2. if some sk' in Sk appears in cond, t, or e, then sk' <_sk sk diff --git a/src/theory/datatypes/options b/src/theory/datatypes/options index 45849858a..d250bee74 100644 --- a/src/theory/datatypes/options +++ b/src/theory/datatypes/options @@ -11,5 +11,7 @@ module DATATYPES "theory/datatypes/options.h" Datatypes theory # cdr( nil ) has no set value. expert-option dtRewriteErrorSel /--disable-dt-rewrite-error-sel bool :default true disable rewriting incorrectly applied selectors to arbitrary ground term +expert-option dtForceAssignment /--dt-force-assignment bool :default false :read-write + force the datatypes solver to give specific values to all datatypes terms before answering sat endmodule diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 9da83ce41..9e4f0de75 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -24,6 +24,7 @@ #include "theory/datatypes/theory_datatypes_type_rules.h" #include "theory/model.h" #include "smt/options.h" +#include "theory/quantifiers/options.h" #include @@ -151,7 +152,7 @@ void TheoryDatatypes::check(Effort e) { } } } - if( !needSplit && mustSpecifyModel() ){ + if( !needSplit && mustSpecifyAssignment() ){ //for the sake of termination, we must choose the constructor of a ground term //NEED GUARENTEE: groundTerm should not contain any subterms of the same type //** TODO: this is probably not good enough, actually need fair enumeration strategy @@ -164,7 +165,7 @@ void TheoryDatatypes::check(Effort e) { } if( needSplit && consIndex!=-1 ) { Node test = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[consIndex].getTester() ), n ); - Trace("dt-split") << "*************Split for possible constructor " << test << " for " << n << endl; + Trace("dt-split") << "*************Split for possible constructor " << dt[consIndex] << " for " << n << endl; test = Rewriter::rewrite( test ); NodeBuilder<> nb(kind::OR); nb << test << test.notNode(); @@ -375,8 +376,13 @@ Node TheoryDatatypes::ppRewrite(TNode in) { void TheoryDatatypes::addSharedTerm(TNode t) { Debug("datatypes") << "TheoryDatatypes::addSharedTerm(): " - << t << endl; - d_equalityEngine.addTriggerTerm(t, THEORY_DATATYPES); + << t << " " << t.getType().isBoolean() << endl; + if( t.getType().isBoolean() ){ + //d_equalityEngine.addTriggerPredicate(t, THEORY_DATATYPES); + }else{ + d_equalityEngine.addTriggerTerm(t, THEORY_DATATYPES); + } + Debug("datatypes") << "TheoryDatatypes::addSharedTerm() finished" << std::endl; } /** propagate */ @@ -489,7 +495,7 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){ Node unifEq = cons1.eqNode( cons2 ); for( int i=0; i<(int)cons1.getNumChildren(); i++ ) { if( cons1[i]!=cons2[i] ){ - Node eq = cons1[i].eqNode( cons2[i] ); + Node eq = cons1[i].getType().isBoolean() ? cons1[i].iffNode( cons2[i] ) : cons1[i].eqNode( cons2[i] ); d_pending.push_back( eq ); d_pending_exp[ eq ] = unifEq; Trace("datatypes-infer") << "DtInfer : " << eq << " by " << unifEq << std::endl; @@ -797,7 +803,7 @@ void TheoryDatatypes::processNewTerm( Node n ){ //see if it is rewritten to be something different Node rn = Rewriter::rewrite( n ); if( rn!=n ){ - Node eq = rn.eqNode( n ); + Node eq = n.getType().isBoolean() ? rn.iffNode( n ) : rn.eqNode( n ); d_pending.push_back( eq ); d_pending_exp[ eq ] = NodeManager::currentNM()->mkConst( true ); Trace("datatypes-infer") << "DtInfer : " << eq << ", trivial" << std::endl; @@ -851,7 +857,7 @@ void TheoryDatatypes::collapseSelectors(){ Node sn = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR, op, cons ); Node s = Rewriter::rewrite( sn ); if( sn!=s ){ - Node eq = s.eqNode( sn ); + Node eq = s.getType().isBoolean() ? s.iffNode( sn ) : s.eqNode( sn ); d_pending.push_back( eq ); d_pending_exp[ eq ] = NodeManager::currentNM()->mkConst( true ); Trace("datatypes-infer") << "DtInfer : " << eq << ", by rewrite" << std::endl; @@ -883,7 +889,7 @@ void TheoryDatatypes::instantiate( EqcInfo* eqc, Node n ){ int index = getLabelIndex( eqc, n ); const Datatype& dt = ((DatatypeType)(tt.getType()).toType()).getDatatype(); //must be finite or have a selector - if( eqc->d_selectors || dt[ index ].isFinite() || mustSpecifyModel() ){ + if( eqc->d_selectors || dt[ index ].isFinite() || mustSpecifyAssignment() ){ //instantiate this equivalence class eqc->d_inst = true; Node tt_cons = getInstantiateCons( tt, dt, index ); @@ -967,9 +973,12 @@ bool TheoryDatatypes::searchForCycle( Node n, Node on, return false; } -bool TheoryDatatypes::mustSpecifyModel(){ - return options::produceModels(); - //return options::finiteModelFind() || options::produceModels(); +bool TheoryDatatypes::mustSpecifyAssignment(){ + //FIXME: the condition finiteModelFind is an over-approximation in this function + // we still may not want to specify assignments for datatypes that are truly infinite + // the fix for this is to correctly compute the cardinality for datatypes containing uninterpered sorts in fmf (i.e. by assuming they are finite) + return options::finiteModelFind() || options::produceModels() || options::dtForceAssignment(); + //return options::produceModels(); //return false; } @@ -980,7 +989,7 @@ bool TheoryDatatypes::mustCommunicateFact( Node n, Node exp ){ // (3) Instantiate : is_C( t ) => t = C( sel_1( t ) ... sel_n( t ) ) //We may need to communicate (3) outwards if the conclusions involve other theories Trace("dt-lemma-debug") << "Compute for " << exp << " => " << n << std::endl; - if( n.getKind()==EQUAL && n[1].getKind()==APPLY_CONSTRUCTOR && exp.getKind()!=EQUAL ){ + if( ( n.getKind()==EQUAL || n.getKind()==IFF) && n[1].getKind()==APPLY_CONSTRUCTOR && exp.getKind()!=EQUAL ){ bool addLemma = false; #if 1 const Datatype& dt = ((DatatypeType)(n[1].getType()).toType()).getDatatype(); @@ -997,13 +1006,15 @@ bool TheoryDatatypes::mustCommunicateFact( Node n, Node exp ){ //check if we have already added this lemma if( std::find( d_inst_lemmas[ n[0] ].begin(), d_inst_lemmas[ n[0] ].end(), n[1] )==d_inst_lemmas[ n[0] ].end() ){ d_inst_lemmas[ n[0] ].push_back( n[1] ); + Trace("dt-lemma-debug") << "Communicate " << n << std::endl; return true; }else{ + Trace("dt-lemma-debug") << "Already communicated " << n << std::endl; return false; } } - Trace("dt-lemma-debug") << "Do not need to communicate " << n << std::endl; } + Trace("dt-lemma-debug") << "Do not need to communicate " << n << std::endl; return false; } diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 9846e80f2..46212ccbf 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -236,7 +236,7 @@ private: * This returns true when the datatypes theory is expected to specify the constructor * type for all equivalence classes. */ - bool mustSpecifyModel(); + bool mustSpecifyAssignment(); /** must communicate fact */ bool mustCommunicateFact( Node n, Node exp ); private: diff --git a/src/theory/quantifiers/inst_strategy_e_matching.h b/src/theory/quantifiers/inst_strategy_e_matching.h index ea22486a6..23f0d8a54 100755 --- a/src/theory/quantifiers/inst_strategy_e_matching.h +++ b/src/theory/quantifiers/inst_strategy_e_matching.h @@ -87,6 +87,9 @@ private: /** generate triggers */ void generateTriggers( Node f ); public: + /** tstrt is the type of triggers to use (maximum depth, minimum depth, or all) + rstrt is the relevance setting for trigger (use only relevant triggers vs. use all) + rgfr is the frequency at which triggers are generated */ InstStrategyAutoGenTriggers( QuantifiersEngine* qe, int tstrt, int rstrt, int rgfr = -1 ) : InstStrategy( qe ), d_tr_strategy( tstrt ), d_rlv_strategy( rstrt ), d_generate_additional( false ){ setRegenerateFrequency( rgfr ); diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index 579c53665..653016d1c 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -60,11 +60,10 @@ void InstantiationEngine::finishInit(){ //d_isup->setPriorityOver( i_agm ); //i_ag->setPriorityOver( i_agm ); } - //CBQI: FIXME //for arithmetic - //if( options::cbqi() ){ - // addInstStrategy( new InstStrategySimplex( d_quantEngine ) ); - //} + if( options::cbqi() ){ + addInstStrategy( new InstStrategySimplex( (arith::TheoryArith*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_ARITH ), d_quantEngine ) ); + } //for datatypes //if( options::cbqi() ){ // addInstStrategy( new InstStrategyDatatypesValue( d_quantEngine ) );