diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-04-08 12:15:27 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-04-08 12:15:33 +0200 |
commit | 4448f36d5c60c05aa2fca3bc760f534cf9926caa (patch) | |
tree | 6c10032e7f2de811b0361fa50f5f4b5355a43d64 /src/theory/quantifiers/conjecture_generator.cpp | |
parent | c871e203705d3e191b8c8028a3f22bca6adb0d16 (diff) |
Make fun-def quantifiers carry the function app they define, make fun-def utilities more robust. Fix bug in conjecture generation for non-parameterized operators.
Diffstat (limited to 'src/theory/quantifiers/conjecture_generator.cpp')
-rwxr-xr-x | src/theory/quantifiers/conjecture_generator.cpp | 11 |
1 files changed, 9 insertions, 2 deletions
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index 520ea5e70..48d3f3902 100755 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -285,8 +285,12 @@ Node ConjectureGenerator::getFreeVar( TypeNode tn, unsigned i ) { while( d_free_var[tn].size()<=i ){
std::stringstream oss;
oss << tn;
+ std::string typ_name = oss.str();
+ while( typ_name[0]=='(' ){
+ typ_name.erase( typ_name.begin() );
+ }
std::stringstream os;
- os << oss.str()[0] << i;
+ os << typ_name[0] << i;
Node x = NodeManager::currentNM()->mkBoundVar( os.str().c_str(), tn );
d_free_var_num[x] = d_free_var[tn].size();
d_free_var[tn].push_back( x );
@@ -1713,7 +1717,9 @@ Node TermGenerator::getTerm( TermGenEnv * s ) { Node f = s->getTgFunc( d_typ, d_status_num );
if( d_children.size()==s->d_func_args[f].size() ){
std::vector< Node > children;
- children.push_back( f );
+ if( s->d_tg_func_param[f] ){
+ children.push_back( f );
+ }
for( unsigned i=0; i<d_children.size(); i++ ){
Node nc = s->d_tg_alloc[d_children[i]].getTerm( s );
if( nc.isNull() ){
@@ -1776,6 +1782,7 @@ void TermGenEnv::collectSignatureInformation() { d_func_kind[it->first] = nn.getKind();
d_typ_tg_funcs[tnull].push_back( it->first );
d_typ_tg_funcs[nn.getType()].push_back( it->first );
+ d_tg_func_param[it->first] = ( nn.getMetaKind() == kind::metakind::PARAMETERIZED );
Trace("sg-rel-sig") << "Will enumerate function applications of : " << it->first << ", #args = " << d_func_args[it->first].size() << ", kind = " << nn.getKind() << std::endl;
getTermDatabase()->computeUfEqcTerms( it->first );
}
|