| 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
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';
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; i<in[0].getNumChildren(); i++ ){
+ if( in[0][i].getType().isDatatype() ){
+ children.push_back( NodeManager::currentNM()->mkNode( 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<TupleSelect>().getIndex()]);
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
// 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);
flushPendingFacts();
}
- if( e == EFFORT_FULL && !d_conflict ) {
+ if( e == EFFORT_FULL && !d_conflict && !d_valuation.needCheck() ) {
//check for cycles
bool addedFact;
do {
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;
}
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 );
}
return EQUALITY_FALSE;
}
}
- return EQUALITY_UNKNOWN;
+ return EQUALITY_FALSE_IN_MODEL;
}
void TheoryDatatypes::computeCareGraph(){
//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;
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 );
+ }
}
}
}
}
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 ){
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 */
}
};/* 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 */
}
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;
+ }
}
}
d_quantEngine->getOutputChannel().lemma( lem );
}
//fairness
- std::vector< Node > mc;
- for( unsigned j=0; j<d_conj->d_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; j<d_conj->d_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 );
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 ){
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;
if( getModelValues( conj->d_candidates, model_values ) ){
//check if we must apply fairness lemmas
std::vector< Node > lems;
- for( unsigned j=0; j<conj->d_candidates.size(); j++ ){
- getMeasureLemmas( conj->d_candidates[j], model_values[j], lems );
+ if( options::ceGuidedInstFair()==CEGQI_FAIR_UF_DT_SIZE ){
+ for( unsigned j=0; j<conj->d_candidates.size(); j++ ){
+ getMeasureLemmas( conj->d_candidates[j], model_values[j], lems );
+ }
}
if( !lems.empty() ){
for( unsigned j=0; j<lems.size(); j++ ){
Trace("cegqi-lemma") << "Measure lemma : " << lems[j] << std::endl;
d_quantEngine->addLemma( 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() );
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;
}
}
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 );
}
}
/** 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
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 */
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
+ 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;
}
}
+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 */
return d_engine->entailmentCheck(mode, lit, params, out);
}
+bool Valuation::needCheck() const{
+ return d_engine->needCheck();
+}
+
}/* CVC4::theory namespace */
}/* CVC4 namespace */
*/
std::pair<bool, Node> 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 */
projects / cvc5.git / commitdiff