From f4046606737f18ed7ffd9da55529e08b704a5b05 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Thu, 16 Oct 2014 12:17:03 +0200 Subject: [PATCH] Add dt.size to datatypes theory. Add option for fairness strategy used by CEGQI. Improve care graph/equality status for datatypes. Only do FULL effort check in datatypes if no other theories used output channel. --- src/parser/smt2/Smt2.g | 4 + src/theory/datatypes/datatypes_rewriter.h | 17 ++++ src/theory/datatypes/kinds | 4 + src/theory/datatypes/theory_datatypes.cpp | 81 +++++++++++-------- src/theory/datatypes/theory_datatypes.h | 2 - .../datatypes/theory_datatypes_type_rules.h | 15 ++++ .../quantifiers/ce_guided_instantiation.cpp | 73 ++++++++++------- .../quantifiers/ce_guided_instantiation.h | 12 --- src/theory/quantifiers/modes.h | 9 +++ src/theory/quantifiers/options | 2 + src/theory/quantifiers/options_handlers.h | 30 +++++++ src/theory/valuation.cpp | 4 + src/theory/valuation.h | 3 + 13 files changed, 182 insertions(+), 74 deletions(-) diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 6fce26484..3d57eebff 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1459,6 +1459,8 @@ builtinOp[CVC4::Kind& kind] | RERANGE_TOK { $kind = CVC4::kind::REGEXP_RANGE; } | RELOOP_TOK { $kind = CVC4::kind::REGEXP_LOOP; } + | DTSIZE_TOK { $kind = CVC4::kind::DT_SIZE; } + | FMFCARD_TOK { $kind = CVC4::kind::CARDINALITY_CONSTRAINT; } // NOTE: Theory operators go here @@ -1858,6 +1860,8 @@ RELOOP_TOK : 're.loop'; RENOSTR_TOK : 're.nostr'; REALLCHAR_TOK : 're.allchar'; +DTSIZE_TOK : 'dt.size'; + FMFCARD_TOK : 'fmf.card'; EMPTYSET_TOK: { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS) }? 'emptyset'; diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h index 37e64ca88..3a41510dd 100644 --- a/src/theory/datatypes/datatypes_rewriter.h +++ b/src/theory/datatypes/datatypes_rewriter.h @@ -159,6 +159,23 @@ public: return RewriteResponse(REWRITE_DONE,gt ); } } + if(in.getKind() == kind::DT_SIZE && in[0].getKind()==kind::APPLY_CONSTRUCTOR ){ + std::vector< Node > children; + for( unsigned i=0; imkNode( kind::DT_SIZE, in[0][i] ) ); + } + } + Node res; + if( !children.empty() ){ + children.push_back( NodeManager::currentNM()->mkConst( Rational(1) ) ); + res = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( kind::PLUS, children ); + }else{ + res = NodeManager::currentNM()->mkConst( Rational(0) ); + } + Trace("datatypes-rewrite") << "DatatypesRewriter::postRewrite: rewrite " << in << " to " << res << std::endl; + return RewriteResponse(REWRITE_AGAIN_FULL, res ); + } if(in.getKind() == kind::TUPLE_SELECT && in[0].getKind() == kind::TUPLE) { return RewriteResponse(REWRITE_DONE, in[0][in.getOperator().getConst().getIndex()]); diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds index faaf78fe4..8c25e2a86 100644 --- a/src/theory/datatypes/kinds +++ b/src/theory/datatypes/kinds @@ -163,4 +163,8 @@ constant RECORD_UPDATE_OP \ parameterized RECORD_UPDATE RECORD_UPDATE_OP 2 "record update; first parameter is a RECORD_UPDATE_OP (which references a field), second is a record term to update, third is the element to store in the record in the given field" typerule RECORD_UPDATE ::CVC4::theory::datatypes::RecordUpdateTypeRule + +operator DT_SIZE 1 "datatypes size" +typerule DT_SIZE ::CVC4::theory::datatypes::DtSizeTypeRule + endtheory diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 145cd32dd..4c37e8889 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -58,6 +58,7 @@ TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out, // The kinds we are treating as function application in congruence d_equalityEngine.addFunctionKind(kind::APPLY_CONSTRUCTOR); d_equalityEngine.addFunctionKind(kind::APPLY_SELECTOR_TOTAL); + d_equalityEngine.addFunctionKind(kind::DT_SIZE); d_equalityEngine.addFunctionKind(kind::APPLY_TESTER); d_equalityEngine.addFunctionKind(kind::APPLY_UF); @@ -147,7 +148,7 @@ void TheoryDatatypes::check(Effort e) { flushPendingFacts(); } - if( e == EFFORT_FULL && !d_conflict ) { + if( e == EFFORT_FULL && !d_conflict && !d_valuation.needCheck() ) { //check for cycles bool addedFact; do { @@ -286,7 +287,7 @@ void TheoryDatatypes::flushPendingFacts(){ Trace("dt-lemma-debug") << "Get explanation..." << std::endl; Node ee_exp = explain( exp ); Trace("dt-lemma-debug") << "Explanation : " << ee_exp << std::endl; - lem = NodeManager::currentNM()->mkNode( IMPLIES, ee_exp, fact ); + lem = NodeManager::currentNM()->mkNode( OR, ee_exp.negate(), fact ); lem = Rewriter::rewrite( lem ); } Trace("dt-lemma") << "Datatypes lemma : " << lem << std::endl; @@ -1027,19 +1028,20 @@ void TheoryDatatypes::addConstructor( Node c, EqcInfo* eqc, Node n ){ } void TheoryDatatypes::collapseSelector( Node s, Node c ) { - Node r = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, s.getOperator(), c ); + Node r; + if( s.getKind()==kind::APPLY_SELECTOR_TOTAL ){ + r = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, s.getOperator(), c ); + }else if( s.getKind()==kind::DT_SIZE ){ + r = NodeManager::currentNM()->mkNode( kind::DT_SIZE, c ); + } Node rr = Rewriter::rewrite( r ); - //if( r!=rr ){ - //Node eq_exp = NodeManager::currentNM()->mkConst(true); - //Node eq = r.getType().isBoolean() ? r.iffNode( rr ) : r.eqNode( rr ); - if( s!=rr ){:: + if( s!=rr ){ Node eq_exp = c.eqNode( s[0] ); Node eq = rr.getType().isBoolean() ? s.iffNode( rr ) : s.eqNode( rr ); - - + Trace("datatypes-infer") << "DtInfer : collapse sel : " << eq << " by " << eq_exp << std::endl; + d_pending.push_back( eq ); d_pending_exp[ eq ] = eq_exp; - Trace("datatypes-infer") << "DtInfer : collapse sel : " << eq << " by " << eq_exp << std::endl; d_infer.push_back( eq ); d_infer_exp.push_back( eq_exp ); } @@ -1056,7 +1058,7 @@ EqualityStatus TheoryDatatypes::getEqualityStatus(TNode a, TNode b){ return EQUALITY_FALSE; } } - return EQUALITY_UNKNOWN; + return EQUALITY_FALSE_IN_MODEL; } void TheoryDatatypes::computeCareGraph(){ @@ -1386,7 +1388,7 @@ void TheoryDatatypes::collectTerms( Node n ) { //eqc->d_selectors = true; } */ - }else if( n.getKind() == APPLY_SELECTOR_TOTAL ){ + }else if( n.getKind() == APPLY_SELECTOR_TOTAL || n.getKind() == DT_SIZE ){ d_selTerms.push_back( n ); //we must also record which selectors exist Debug("datatypes") << " Found selector " << n << endl; @@ -1400,6 +1402,15 @@ void TheoryDatatypes::collectTerms( Node n ) { EqcInfo* eqc = getOrMakeEqcInfo( rep, true ); //add it to the eqc info addSelector( n, eqc, rep ); + + if( n.getKind() == DT_SIZE ){ + Node conc = NodeManager::currentNM()->mkNode( LEQ, NodeManager::currentNM()->mkConst( Rational(0) ), n ); + //must be non-negative + Trace("datatypes-infer") << "DtInfer : non-negative size : " << conc << std::endl; + d_pending.push_back( conc ); + d_pending_exp[ conc ] = d_true; + d_infer.push_back( conc ); + } } } } @@ -1731,35 +1742,39 @@ bool TheoryDatatypes::mustSpecifyAssignment(){ } bool TheoryDatatypes::mustCommunicateFact( Node n, Node exp ){ - //the datatypes decision procedure makes 3 "internal" inferences apart from the equality engine : + //the datatypes decision procedure makes 5 "internal" inferences apart from the equality engine : // (1) Unification : C( t1...tn ) = C( s1...sn ) => ti = si // (2) Label : ~is_C1( t ) ... ~is_C{i-1}( t ) ~is_C{i+1}( t ) ... ~is_Cn( t ) => is_Ci( t ) // (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 + // (4) collapse selector : S( C( t1...tn ) ) = t' + // (5) collapse term size : size( C( t1...tn ) ) = 1 + size( t1 ) + ... + size( tn ) + // (6) non-negative size : 0 <= size( t ) + //We may need to communicate (3) outwards if the conclusions involve other theories. Also communicate (5) and (6). Trace("dt-lemma-debug") << "Compute for " << exp << " => " << n << std::endl; bool addLemma = false; if( ( n.getKind()==EQUAL || n.getKind()==IFF) && n[1].getKind()==APPLY_CONSTRUCTOR && exp.getKind()!=EQUAL ){ -#if 1 const Datatype& dt = ((DatatypeType)(n[1].getType()).toType()).getDatatype(); addLemma = dt.involvesExternalType(); -#else - for( int j=0; j<(int)n[1].getNumChildren(); j++ ){ - if( !DatatypesRewriter::isTermDatatype( n[1][j] ) ){ - addLemma = true; - break; - } - } -#endif - if( addLemma ){ - //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; - } + //for( int j=0; j<(int)n[1].getNumChildren(); j++ ){ + // if( !DatatypesRewriter::isTermDatatype( n[1][j] ) ){ + // addLemma = true; + // break; + // } + //} + }else if( n.getKind()==EQUAL && ( n[0].getKind()==DT_SIZE || n[1].getKind()==DT_SIZE ) ){ + addLemma = true; + }else if( n.getKind()==LEQ ){ + addLemma = true; + } + if( addLemma ){ + //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; } } //else if( exp.getKind()==APPLY_TESTER ){ diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 74d10e754..d698e80c9 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -138,8 +138,6 @@ private: eq::EqualityEngine d_equalityEngine; /** information necessary for equivalence classes */ std::map< Node, EqcInfo* > d_eqc_info; - /** selector applications */ - //BoolMap d_selector_apps; /** map from nodes to their instantiated equivalent for each constructor type */ std::map< Node, std::map< int, Node > > d_inst_map; /** which instantiation lemmas we have sent */ diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h index 8ce8ee7df..84be5238d 100644 --- a/src/theory/datatypes/theory_datatypes_type_rules.h +++ b/src/theory/datatypes/theory_datatypes_type_rules.h @@ -551,6 +551,21 @@ struct RecordProperties { } };/* struct RecordProperties */ +class DtSizeTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + if( check ) { + TypeNode t = n[0].getType(check); + if (!t.isDatatype()) { + throw TypeCheckingExceptionPrivate(n, "expecting datatype size term to have datatype argument."); + } + } + return nodeManager->integerType(); + } +};/* class DtSizeTypeRule */ + + }/* CVC4::theory::datatypes namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index 90e7a274a..dddbee73b 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -50,19 +50,23 @@ void CegInstantiation::CegConjecture::initializeGuard( QuantifiersEngine * qe ){ } Node CegInstantiation::CegConjecture::getLiteral( QuantifiersEngine * qe, int i ) { - std::map< int, Node >::iterator it = d_lits.find( i ); - if( it==d_lits.end() ){ - Node lit = NodeManager::currentNM()->mkNode( LEQ, d_measure_term, NodeManager::currentNM()->mkConst( Rational( i ) ) ); - lit = Rewriter::rewrite( lit ); - d_lits[i] = lit; - - Node lem = NodeManager::currentNM()->mkNode( kind::OR, lit, lit.negate() ); - Trace("cegqi-lemma") << "Fairness split : " << lem << std::endl; - qe->getOutputChannel().lemma( lem ); - qe->getOutputChannel().requirePhase( lit, true ); - return lit; + if( d_measure_term.isNull() ){ + return Node::null(); }else{ - return it->second; + std::map< int, Node >::iterator it = d_lits.find( i ); + if( it==d_lits.end() ){ + Node lit = NodeManager::currentNM()->mkNode( LEQ, d_measure_term, NodeManager::currentNM()->mkConst( Rational( i ) ) ); + lit = Rewriter::rewrite( lit ); + d_lits[i] = lit; + + Node lem = NodeManager::currentNM()->mkNode( kind::OR, lit, lit.negate() ); + Trace("cegqi-lemma") << "Fairness split : " << lem << std::endl; + qe->getOutputChannel().lemma( lem ); + qe->getOutputChannel().requirePhase( lit, true ); + return lit; + }else{ + return it->second; + } } } @@ -110,18 +114,26 @@ void CegInstantiation::registerQuantifier( Node q ) { d_quantEngine->getOutputChannel().lemma( lem ); } //fairness - std::vector< Node > mc; - for( unsigned j=0; jd_candidates.size(); j++ ){ - TypeNode tn = d_conj->d_candidates[j].getType(); - registerMeasuredType( tn ); - std::map< TypeNode, Node >::iterator it = d_uf_measure.find( tn ); - if( it!=d_uf_measure.end() ){ - mc.push_back( NodeManager::currentNM()->mkNode( APPLY_UF, it->second, d_conj->d_candidates[j] ) ); + if( options::ceGuidedInstFair()!=CEGQI_FAIR_NONE ){ + std::vector< Node > mc; + for( unsigned j=0; jd_candidates.size(); j++ ){ + TypeNode tn = d_conj->d_candidates[j].getType(); + if( options::ceGuidedInstFair()==CEGQI_FAIR_DT_SIZE ){ + if( tn.isDatatype() ){ + mc.push_back( NodeManager::currentNM()->mkNode( DT_SIZE, d_conj->d_candidates[j] ) ); + } + }else if( options::ceGuidedInstFair()==CEGQI_FAIR_UF_DT_SIZE ){ + registerMeasuredType( tn ); + std::map< TypeNode, Node >::iterator it = d_uf_measure.find( tn ); + if( it!=d_uf_measure.end() ){ + mc.push_back( NodeManager::currentNM()->mkNode( APPLY_UF, it->second, d_conj->d_candidates[j] ) ); + } + } + } + if( !mc.empty() ){ + d_conj->d_measure_term = mc.size()==1 ? mc[0] : NodeManager::currentNM()->mkNode( PLUS, mc ); + Trace("cegqi") << "Measure term is : " << d_conj->d_measure_term << std::endl; } - } - if( !mc.empty() ){ - d_conj->d_measure_term = mc.size()==1 ? mc[0] : NodeManager::currentNM()->mkNode( PLUS, mc ); - Trace("cegqi") << "Measure term is : " << d_conj->d_measure_term << std::endl; } }else{ Assert( d_conj->d_quant==q ); @@ -154,7 +166,7 @@ Node CegInstantiation::getNextDecisionRequest() { return d_conj->d_guard; } //enforce fairness - if( d_conj->isAssigned() ){ + if( d_conj->isAssigned() && options::ceGuidedInstFair()!=CEGQI_FAIR_NONE ){ Node lit = d_conj->getLiteral( d_quantEngine, d_conj->d_curr_lit.get() ); if( d_quantEngine->getValuation().hasSatValue( lit, value ) ) { if( !value ){ @@ -180,7 +192,9 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) { Trace("cegqi-engine") << conj->d_candidates[i] << " "; } Trace("cegqi-engine") << std::endl; - Trace("cegqi-engine") << " * Current term size : " << conj->d_curr_lit.get() << std::endl; + if( options::ceGuidedInstFair()!=CEGQI_FAIR_NONE ){ + Trace("cegqi-engine") << " * Current term size : " << conj->d_curr_lit.get() << std::endl; + } if( conj->d_ce_sk.empty() ){ Trace("cegqi-engine") << " *** Check candidate phase..." << std::endl; @@ -190,14 +204,17 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) { if( getModelValues( conj->d_candidates, model_values ) ){ //check if we must apply fairness lemmas std::vector< Node > lems; - for( unsigned j=0; jd_candidates.size(); j++ ){ - getMeasureLemmas( conj->d_candidates[j], model_values[j], lems ); + if( options::ceGuidedInstFair()==CEGQI_FAIR_UF_DT_SIZE ){ + for( unsigned j=0; jd_candidates.size(); j++ ){ + getMeasureLemmas( conj->d_candidates[j], model_values[j], lems ); + } } if( !lems.empty() ){ for( unsigned j=0; jaddLemma( lems[j] ); } + Trace("cegqi-engine") << " ...refine size." << std::endl; }else{ //must get a counterexample to the value of the current candidate Node inst = conj->d_base_inst.substitute( conj->d_candidates.begin(), conj->d_candidates.end(), model_values.begin(), model_values.end() ); @@ -210,6 +227,7 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) { Trace("cegqi-lemma") << "Counterexample lemma : " << inst_sk << std::endl; d_quantEngine->addLemma( NodeManager::currentNM()->mkNode( OR, q.negate(), inst_sk.negate() ) ); conj->d_ce_sk.push_back( inst[0] ); + Trace("cegqi-engine") << " ...find counterexample." << std::endl; } } @@ -233,6 +251,7 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) { model_values.begin(), model_values.end() ); Node lem = NodeManager::currentNM()->mkNode( OR, conj->d_guard.negate(), inst_ce_refine ); Trace("cegqi-lemma") << "Candidate refinement lemma : " << lem << std::endl; + Trace("cegqi-engine") << " ...refine candidate." << std::endl; d_quantEngine->addLemma( lem ); } } diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h index cb1825377..2502416bd 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.h +++ b/src/theory/quantifiers/ce_guided_instantiation.h @@ -68,18 +68,6 @@ private: /** allocate literal */ Node getLiteral( QuantifiersEngine * qe, int i ); }; - class CegFairness { - public: - CegFairness( context::Context* c ); - /** which conjecture we are looking at */ - CegConjecture * d_conj; - /** the cardinality literals */ - std::map< int, Node > d_lits; - /** current cardinality */ - context::CDO< int > d_curr_lit; - /** allocate literal */ - Node getLiteral( int i ); - }; /** the quantified formula stating the synthesis conjecture */ CegConjecture * d_conj; private: //for enforcing fairness diff --git a/src/theory/quantifiers/modes.h b/src/theory/quantifiers/modes.h index 993ac5536..53c04cfe8 100644 --- a/src/theory/quantifiers/modes.h +++ b/src/theory/quantifiers/modes.h @@ -125,6 +125,15 @@ typedef enum { PRENEX_NONE, } PrenexQuantMode; +typedef enum { + /** enforce fairness by UF corresponding to datatypes size */ + CEGQI_FAIR_UF_DT_SIZE, + /** enforce fairness by datatypes size */ + CEGQI_FAIR_DT_SIZE, + /** do not use fair strategy for CEGQI */ + CEGQI_FAIR_NONE, +} CegqiFairMode; + }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index d608f0820..1cab2f9d8 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -178,5 +178,7 @@ option conjectureUeeIntro --conjecture-gen-uee-intro bool :default false option ceGuidedInst --cegqi bool :default false counterexample guided quantifier instantiation +option ceGuidedInstFair --cegqi-fair=MODE CVC4::theory::quantifiers::CegqiFairMode :default CVC4::theory::quantifiers::CEGQI_FAIR_UF_DT_SIZE :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToCegqiFairMode :handler-include "theory/quantifiers/options_handlers.h" + if and how to apply fairness for cegqi endmodule diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h index 9558aa0e0..be74fffab 100644 --- a/src/theory/quantifiers/options_handlers.h +++ b/src/theory/quantifiers/options_handlers.h @@ -178,6 +178,20 @@ none \n\ + Do no prenex nested quantifiers. \n\ \n\ "; +static const std::string cegqiFairModeHelp = "\ +Modes for enforcing fairness for counterexample guided quantifier instantion, supported by --cegqi-fair:\n\ +\n\ +default \n\ ++ Default, enforce fairness using an uninterpreted function for datatypes size.\n\ +\n\ +dt-size \n\ ++ Enforce fairness using size theory operator.\n\ +\n\ +none \n\ ++ Do not enforce fairness. \n\ +\n\ +"; + inline InstWhenMode stringToInstWhenMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { if(optarg == "pre-full") { return INST_WHEN_PRE_FULL; @@ -355,6 +369,22 @@ inline PrenexQuantMode stringToPrenexQuantMode(std::string option, std::string o } } +inline CegqiFairMode stringToCegqiFairMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { + if(optarg == "default" || optarg == "uf-dt-size" ) { + return CEGQI_FAIR_UF_DT_SIZE; + } else if(optarg == "dt-size") { + return CEGQI_FAIR_DT_SIZE; + } else if(optarg == "none") { + return CEGQI_FAIR_NONE; + } else if(optarg == "help") { + puts(cegqiFairModeHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --cegqi-fair: `") + + optarg + "'. Try --cegqi-fair help."); + } +} + }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/valuation.cpp b/src/theory/valuation.cpp index b2d7f4b21..7407086c2 100644 --- a/src/theory/valuation.cpp +++ b/src/theory/valuation.cpp @@ -103,5 +103,9 @@ std::pair Valuation::entailmentCheck(theory::TheoryOfMode mode, TNod return d_engine->entailmentCheck(mode, lit, params, out); } +bool Valuation::needCheck() const{ + return d_engine->needCheck(); +} + }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/valuation.h b/src/theory/valuation.h index 448d055d4..540ebd8fc 100644 --- a/src/theory/valuation.h +++ b/src/theory/valuation.h @@ -135,6 +135,9 @@ public: */ std::pair entailmentCheck(theory::TheoryOfMode mode, TNode lit, const theory::EntailmentCheckParameters* params = NULL, theory::EntailmentCheckSideEffects* out = NULL); + /** need check ? */ + bool needCheck() const; + };/* class Valuation */ }/* CVC4::theory namespace */ -- 2.30.2