diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-05-16 17:30:59 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-05-16 17:30:59 -0500 |
commit | 246fffffafba07aaeadd0d0c99a2e1c4b589a63c (patch) | |
tree | 5d2b41e264fc2039da115556befa7fe487a12bb7 /src/theory/quantifiers_engine.cpp | |
parent | f58c881034d3b0193dfee8fabf451cc0e9ea20ab (diff) |
Enable --sygus-direct-eval by default, limit to terms that do not induce Boolean structure. Minor fixes for bitvectors: rewrite SDIV to total operators when options::bitvectorDivByZeroConst is true, fix collectModelInfo when fullModel=false. Lift ITEs in sygus search. Fix sygus initialization related to cbqi.
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 21be4ea4f..8984cc5f4 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -655,6 +655,7 @@ bool QuantifiersEngine::registerQuantifier( Node f ){ for( unsigned i=0; i<d_modules.size(); i++ ){ d_modules[i]->registerQuantifier( f ); } + //TODO: remove this Node ceBody = d_term_db->getInstConstantBody( f ); //also register it with the strong solver //if( options::finiteModelFind() ){ @@ -887,6 +888,7 @@ Node QuantifiersEngine::getInstantiation( Node q, std::vector< Node >& vars, std Node body; //process partial instantiation if necessary if( d_term_db->d_vars[q].size()!=vars.size() ){ + Assert( vars.size()==terms.size() ); body = q[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ); std::vector< Node > uninst_vars; //doing a partial instantiation, must add quantifier for all uninstantiated variables @@ -901,6 +903,7 @@ Node QuantifiersEngine::getInstantiation( Node q, std::vector< Node >& vars, std Trace("partial-inst") << " : " << body << std::endl; }else{ if( options::cbqi() ){ + Assert( vars.size()==terms.size() ); body = q[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ); }else{ //do optimized version @@ -933,6 +936,7 @@ Node QuantifiersEngine::getInstantiation( Node q, InstMatch& m, bool doVts ){ } Node QuantifiersEngine::getInstantiation( Node q, std::vector< Node >& terms, bool doVts ) { + Assert( d_term_db->d_vars.find( q )!=d_term_db->d_vars.end() ); return getInstantiation( q, d_term_db->d_vars[q], terms, doVts ); } |