From 9867d5a61ccde30f7e4616a652ef86a9b15ae6d8 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Thu, 22 Jan 2015 09:40:51 +0100 Subject: [PATCH] Do not drop patterns during boolean term rewriting. Narrow sygus search space based on commutative operators. --- src/smt/boolean_terms.cpp | 28 ++-- src/smt/smt_engine.cpp | 7 + src/theory/datatypes/datatypes_sygus.cpp | 139 ++++++++++-------- src/theory/datatypes/datatypes_sygus.h | 3 +- src/theory/datatypes/theory_datatypes.cpp | 7 +- .../quantifiers/ce_guided_instantiation.cpp | 3 +- src/theory/quantifiers/options | 3 +- 7 files changed, 114 insertions(+), 76 deletions(-) diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp index 7ab590d89..54a6b5416 100644 --- a/src/smt/boolean_terms.cpp +++ b/src/smt/boolean_terms.cpp @@ -816,7 +816,13 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa } Node boundVarList = nm->mkNode(kind::BOUND_VAR_LIST, boundVars); Node body = rewriteBooleanTermsRec(top[1], theory::THEORY_BOOL, quantBoolVars); - Node quant = nm->mkNode(top.getKind(), boundVarList, body); + Node quant; + if( top.getNumChildren()==3 ){ + Node ipl = rewriteBooleanTermsRec(top[2], theory::THEORY_BOOL, quantBoolVars); + quant = nm->mkNode(top.getKind(), boundVarList, body, ipl ); + }else{ + quant = nm->mkNode(top.getKind(), boundVarList, body); + } Debug("bt") << "rewrote quantifier to -> " << quant << endl; d_termCache[make_pair(top, theory::THEORY_BOOL)] = quant; d_termCache[make_pair(top, theory::THEORY_BUILTIN)] = quant.iteNode(d_tt, d_ff); @@ -847,16 +853,16 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa k != kind::RECORD_SELECT && k != kind::RECORD_UPDATE && k != kind::DIVISIBLE && - // Theory parametric functions go here - k != kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR && - k != kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT && - k != kind::FLOATINGPOINT_TO_FP_REAL && - k != kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR && - k != kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR && - k != kind::FLOATINGPOINT_TO_UBV && - k != kind::FLOATINGPOINT_TO_SBV && - k != kind::FLOATINGPOINT_TO_REAL - ) { + // Theory parametric functions go here + k != kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR && + k != kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT && + k != kind::FLOATINGPOINT_TO_FP_REAL && + k != kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR && + k != kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR && + k != kind::FLOATINGPOINT_TO_UBV && + k != kind::FLOATINGPOINT_TO_SBV && + k != kind::FLOATINGPOINT_TO_REAL + ) { Debug("bt") << "rewriting: " << top.getOperator() << endl; result.top() << rewriteBooleanTermsRec(top.getOperator(), theory::THEORY_BUILTIN, quantBoolVars); Debug("bt") << "got: " << result.top().getOperator() << endl; diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index ee09359ad..0e1be30de 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1344,6 +1344,13 @@ void SmtEngine::setDefaults() { } } } + + //apply counterexample guided instantiation options + if( options::ceGuidedInst() ){ + if( !options::quantConflictFind.wasSetByUser() ){ + options::quantConflictFind.set( false ); + } + } //implied options... if( options::recurseCbqi() ){ diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp index cad4aaa48..8192ec067 100644 --- a/src/theory/datatypes/datatypes_sygus.cpp +++ b/src/theory/datatypes/datatypes_sygus.cpp @@ -21,6 +21,8 @@ #include "theory/bv/theory_bv_utils.h" #include "util/bitvector.h" +#include "theory/quantifiers/options.h" + using namespace CVC4; using namespace CVC4::kind; using namespace CVC4::context; @@ -55,10 +57,10 @@ int SygusSplit::getConstArg( TypeNode tn, Node n ){ return -1; } -bool SygusSplit::hasKind( TypeNode tn, Kind k ) { +bool SygusSplit::hasKind( TypeNode tn, Kind k ) { return getKindArg( tn, k )!=-1; } -bool SygusSplit::hasConst( TypeNode tn, Node n ) { +bool SygusSplit::hasConst( TypeNode tn, Node n ) { return getConstArg( tn, n )!=-1; } @@ -66,7 +68,7 @@ bool SygusSplit::isKindArg( TypeNode tn, int i ) { Assert( isRegistered( tn ) ); std::map< TypeNode, std::map< int, Kind > >::iterator itt = d_arg_kind.find( tn ); if( itt!=d_arg_kind.end() ){ - return itt->second.find( i )!=itt->second.end(); + return itt->second.find( i )!=itt->second.end(); }else{ return false; } @@ -76,79 +78,94 @@ bool SygusSplit::isConstArg( TypeNode tn, int i ) { Assert( isRegistered( tn ) ); std::map< TypeNode, std::map< int, Node > >::iterator itt = d_arg_const.find( tn ); if( itt!=d_arg_const.end() ){ - return itt->second.find( i )!=itt->second.end(); + return itt->second.find( i )!=itt->second.end(); }else{ return false; } } -void SygusSplit::getSygusSplits( Node n, const Datatype& dt, std::vector< Node >& splits ) { +void SygusSplit::getSygusSplits( Node n, const Datatype& dt, std::vector< Node >& splits, std::vector< Node >& lemmas ) { Assert( dt.isSygus() ); - Trace("sygus-split") << "Get sygus splits " << n << std::endl; - - //get the kinds for child datatype - TypeNode tnn = n.getType(); - registerSygusType( tnn, dt ); - - //get parent information, if possible - int csIndex = -1; - int sIndex = -1; - if( n.getKind()==APPLY_SELECTOR_TOTAL ){ - Node op = n.getOperator(); - Expr selectorExpr = op.toExpr(); - const Datatype& pdt = Datatype::datatypeOf(selectorExpr); - Assert( pdt.isSygus() ); - csIndex = Datatype::cindexOf(selectorExpr); - sIndex = Datatype::indexOf(selectorExpr); - TypeNode tnnp = n[0].getType(); - //register the constructors that are redundant children of argument sIndex of constructor index csIndex of dt - registerSygusTypeConstructorArg( tnn, dt, tnnp, pdt, csIndex, sIndex ); - - - //relationships between arguments - /* - if( isKindArg( tnnp, csIndex ) ){ - Kind parentKind = d_arg_kind[tnnp][csIndex]; - if( isComm( parentKind ) ){ - //if commutative, normalize based on term ordering (the constructor index of left arg must be less than or equal to the right arg) - Trace("sygus-split-debug") << "Commutative operator : " << parentKind << std::endl; - if( pdt[csIndex].getNumArgs()==2 ){ - TypeNode tn1 = TypeNode::fromType( ((SelectorType)pdt[csIndex][0].getType()).getRangeType() ); - TypeNode tn2 = TypeNode::fromType( ((SelectorType)pdt[csIndex][1].getType()).getRangeType() ); - if( tn1==tn2 ){ - if( sIndex==1 ){ + if( d_splits.find( n )==d_splits.end() ){ + Trace("sygus-split") << "Get sygus splits " << n << std::endl; + //get the kinds for child datatype + TypeNode tnn = n.getType(); + registerSygusType( tnn, dt ); + + //get parent information, if possible + int csIndex = -1; + int sIndex = -1; + Node onComm; + if( n.getKind()==APPLY_SELECTOR_TOTAL ){ + Node op = n.getOperator(); + Expr selectorExpr = op.toExpr(); + const Datatype& pdt = Datatype::datatypeOf(selectorExpr); + Assert( pdt.isSygus() ); + csIndex = Datatype::cindexOf(selectorExpr); + sIndex = Datatype::indexOf(selectorExpr); + TypeNode tnnp = n[0].getType(); + //register the constructors that are redundant children of argument sIndex of constructor index csIndex of dt + registerSygusTypeConstructorArg( tnn, dt, tnnp, pdt, csIndex, sIndex ); + + + //relationships between arguments + if( isKindArg( tnnp, csIndex ) ){ + Kind parentKind = d_arg_kind[tnnp][csIndex]; + if( sIndex==1 && isComm( parentKind ) ){ + //if commutative, normalize based on term ordering (the constructor index of left arg must be less than or equal to the right arg) + Trace("sygus-split-debug") << "Commutative operator : " << parentKind << std::endl; + if( pdt[csIndex].getNumArgs()==2 ){ + TypeNode tn1 = TypeNode::fromType( ((SelectorType)pdt[csIndex][0].getType()).getRangeType() ); + TypeNode tn2 = TypeNode::fromType( ((SelectorType)pdt[csIndex][1].getType()).getRangeType() ); + if( tn1==tn2 ){ registerSygusTypeConstructorArg( tnn, dt, tnnp, pdt, csIndex, 0 ); - } - for( unsigned i=1; i lem_c; - for( unsigned j=0; jmkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( pdt[csIndex][0].getSelector() ), n[0] ); } } } } + } - */ - } - for( unsigned i=0; i lem_c; + for( unsigned j=0; j<=i; j++ ){ + if( d_sygus_pc_nred[tnn][csIndex][0][i] ){ + lem_c.push_back( DatatypesRewriter::mkTester( onComm, j, dt ) ); + } + } + Assert( !lem_c.empty() ); + Node commStr = lem_c.size()==1 ? lem_c[0] : NodeManager::currentNM()->mkNode( OR, lem_c ); + Trace("sygus-nf") << "...strengthen " << test << " based on commutatitivity : " << commStr << std::endl; + test = NodeManager::currentNM()->mkNode( AND, test, commStr ); + } + } + d_splits[n].push_back( test ); + Trace("sygus-split-debug2") << "SUCCESS" << std::endl; + }else{ + Trace("sygus-split-debug2") << "redundant argument" << std::endl; + } + }else{ + Trace("sygus-split-debug2") << "redundant operator" << std::endl; } } + Assert( !d_splits[n].empty() ); } - Assert( !splits.empty() ); + //copy to splits + splits.insert( splits.end(), d_splits[n].begin(), d_splits[n].end() ); } void SygusSplit::registerSygusType( TypeNode tn, const Datatype& dt ) { @@ -172,7 +189,7 @@ void SygusSplit::registerSygusType( TypeNode tn, const Datatype& dt ) { } Trace("sygus-split") << std::endl; } - + //compute the redundant operators for( unsigned i=0; i > d_splits; std::map< TypeNode, std::vector< bool > > d_sygus_nred; std::map< TypeNode, std::map< int, std::map< int, std::vector< bool > > > > d_sygus_pc_nred; //information for builtin types @@ -75,7 +76,7 @@ private: int getFirstArgOccurrence( const DatatypeConstructor& c, const Datatype& dt ); public: /** get sygus splits */ - void getSygusSplits( Node n, const Datatype& dt, std::vector< Node >& splits ); + void getSygusSplits( Node n, const Datatype& dt, std::vector< Node >& splits, std::vector< Node >& lemmas ); }; diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index bbc8837b9..82804e565 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -246,7 +246,12 @@ void TheoryDatatypes::check(Effort e) { Trace("dt-split") << "*************Split for constructors on " << n << endl; std::vector< Node > children; if( dt.isSygus() && d_sygus_split ){ - d_sygus_split->getSygusSplits( n, dt, children ); + std::vector< Node > lemmas; + d_sygus_split->getSygusSplits( n, dt, children, lemmas ); + for( unsigned i=0; ilemma( lemmas[i] ); + } }else{ for( unsigned i=0; i& d ) { d.push_back( n ); } } - + CegInstantiation::CegConjecture::CegConjecture( context::Context* c ) : d_active( c, false ), d_infeasible( c, false ), d_curr_lit( c, 0 ){ d_refine_count = 0; } @@ -72,6 +72,7 @@ Node CegInstantiation::CegConjecture::getLiteral( QuantifiersEngine * qe, int i }else{ 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 ) ) ); lit = Rewriter::rewrite( lit ); d_lits[i] = lit; diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index cebc5f245..afa894473 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -200,7 +200,8 @@ option sygusDecompose --sygus-decompose bool :default false decompose single invocation synthesis conjectures option sygusNormalForm --sygus-normal-form 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 option localTheoryExt --local-t-ext bool :default false do instantiation based on local theory extensions -- 2.30.2