From 97d43d56d74f3af68d1d022c66ee158a41b24757 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 23 Jan 2015 14:53:19 +0100 Subject: CEGQI fairness based on term height. Fix sygus-nf fairness bug for wrongly applied selectors. --- src/theory/quantifiers/ce_guided_instantiation.cpp | 17 ++++++++++++++++- src/theory/quantifiers/modes.h | 2 ++ src/theory/quantifiers/options | 2 +- src/theory/quantifiers/options_handlers.h | 5 +++++ 4 files changed, 24 insertions(+), 2 deletions(-) (limited to 'src/theory/quantifiers') diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index b1850b373..bb53c9cfb 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -73,7 +73,8 @@ Node CegInstantiation::CegConjecture::getLiteral( QuantifiersEngine * qe, int i std::map< int, Node >::iterator it = d_lits.find( i ); if( it==d_lits.end() ){ Trace("cegqi-engine") << "******* CEGQI : allocate size literal " << i << std::endl; - Node lit = NodeManager::currentNM()->mkNode( LEQ, d_measure_term, NodeManager::currentNM()->mkConst( Rational( i ) ) ); + Node c = NodeManager::currentNM()->mkConst( Rational( i ) ); + Node lit = NodeManager::currentNM()->mkNode( LEQ, d_measure_term, c ); lit = Rewriter::rewrite( lit ); d_lits[i] = lit; @@ -81,6 +82,17 @@ Node CegInstantiation::CegConjecture::getLiteral( QuantifiersEngine * qe, int i Trace("cegqi-lemma") << "Fairness split : " << lem << std::endl; qe->getOutputChannel().lemma( lem ); qe->getOutputChannel().requirePhase( lit, true ); + + if( options::ceGuidedInstFair()==CEGQI_FAIR_DT_HEIGHT_PRED ){ + //implies height bounds on each candidate variable + std::vector< Node > lem_c; + for( unsigned j=0; jmkNode( DT_HEIGHT_BOUND, d_candidates[j], c ) ); + } + Node hlem = NodeManager::currentNM()->mkNode( OR, lit.negate(), lem_c.size()==1 ? lem_c[0] : NodeManager::currentNM()->mkNode( AND, lem_c ) ); + Trace("cegqi-lemma") << "Fairness expansion (dt-height-pred) : " << hlem << std::endl; + qe->getOutputChannel().lemma( hlem ); + } return lit; }else{ return it->second; @@ -158,6 +170,9 @@ void CegInstantiation::registerQuantifier( Node q ) { if( it!=d_uf_measure.end() ){ mc.push_back( NodeManager::currentNM()->mkNode( APPLY_UF, it->second, d_conj->d_candidates[j] ) ); } + }else if( options::ceGuidedInstFair()==CEGQI_FAIR_DT_HEIGHT_PRED ){ + //measure term is a fresh constant + mc.push_back( NodeManager::currentNM()->mkSkolem( "K", NodeManager::currentNM()->integerType() ) ); } } if( !mc.empty() ){ diff --git a/src/theory/quantifiers/modes.h b/src/theory/quantifiers/modes.h index 5e692ace1..a6c52274f 100644 --- a/src/theory/quantifiers/modes.h +++ b/src/theory/quantifiers/modes.h @@ -128,6 +128,8 @@ typedef enum { CEGQI_FAIR_UF_DT_SIZE, /** enforce fairness by datatypes size */ CEGQI_FAIR_DT_SIZE, + /** enforce fairness by datatypes height bound */ + CEGQI_FAIR_DT_HEIGHT_PRED, /** do not use fair strategy for CEGQI */ CEGQI_FAIR_NONE, } CegqiFairMode; diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 009a0ada6..560e29c3b 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -198,7 +198,7 @@ option ceGuidedInstFair --cegqi-fair=MODE CVC4::theory::quantifiers::CegqiFairMo if and how to apply fairness for cegqi option sygusDecompose --sygus-decompose bool :default false decompose single invocation synthesis conjectures -option sygusNormalForm --sygus-normal-form bool :default true +option sygusNormalForm --sygus-nf bool :default true only search for sygus builtin terms that are in normal form option sygusNormalFormArg --sygus-nf-arg bool :default true account for relationship between arguments of operations in sygus normal form diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h index e9f85d454..fdfad21b9 100644 --- a/src/theory/quantifiers/options_handlers.h +++ b/src/theory/quantifiers/options_handlers.h @@ -184,6 +184,9 @@ uf-dt-size \n\ default | dt-size \n\ + Default, enforce fairness using size theory operator.\n\ \n\ +dt-height-bound \n\ ++ Enforce fairness by height bound predicate.\n\ +\n\ none \n\ + Do not enforce fairness. \n\ \n\ @@ -379,6 +382,8 @@ inline CegqiFairMode stringToCegqiFairMode(std::string option, std::string optar return CEGQI_FAIR_UF_DT_SIZE; } else if(optarg == "default" || optarg == "dt-size") { return CEGQI_FAIR_DT_SIZE; + } else if(optarg == "dt-height-bound" ){ + return CEGQI_FAIR_DT_HEIGHT_PRED; } else if(optarg == "none") { return CEGQI_FAIR_NONE; } else if(optarg == "help") { -- cgit v1.2.3