diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-08-01 17:22:11 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-08-01 17:22:11 +0200 |
commit | 86ad2ca93048844eedcafd2a2dadc43ef85dfb32 (patch) | |
tree | 69e4b02df3f06e090a668f01fbf8a18438d927c1 /src/parser | |
parent | 8f4e966ae0c0f42e595e1c603cb7c3f779b713ef (diff) |
Simplification/improvement to solving deltas in LRA cbqi. Bug fix sygus datatypes.
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/smt2/smt2.cpp | 6 |
1 files changed, 1 insertions, 5 deletions
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index cc3b09cfe..7e621f56b 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -545,11 +545,7 @@ void Smt2::mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::strin std::map< Type, std::vector< DatatypeConstructorArg > > sels; //types for each of the variables for( unsigned i=0; i<sygus_vars.size(); i++ ){ - Type t = sygus_vars[i].getType(); - if( !t.isBoolean() && std::find( types.begin(), types.end(), t )==types.end() ){ - Debug("parser-sygus") << "...will make grammar for " << t << std::endl; - types.push_back( t ); - } + collectSygusGrammarTypesFor( sygus_vars[i].getType(), types, sels ); } //types connected to range collectSygusGrammarTypesFor( range, types, sels ); |