From: ajreynol Date: Wed, 4 Jan 2017 21:28:24 +0000 (-0600) Subject: Fix for tff type declarations inTPTP parser, fixes bug 748. Other minor changes. X-Git-Tag: cvc5-1.0.0~5924 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5552e43454c3b45ae8c7b35a822ac4b39adca72f;p=cvc5.git Fix for tff type declarations inTPTP parser, fixes bug 748. Other minor changes. --- diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g index 73dcfa6cb..414c2f6b0 100644 --- a/src/parser/tptp/Tptp.g +++ b/src/parser/tptp/Tptp.g @@ -803,6 +803,9 @@ parseType[CVC4::Type& type] // non-function types simpleType[CVC4::Type& type] +@declarations { + std::string name; +} : DEFINED_SYMBOL { std::string s = AntlrInput::tokenText($DEFINED_SYMBOL); if(s == "\$i") type = PARSER_STATE->d_unsorted; @@ -813,8 +816,8 @@ simpleType[CVC4::Type& type] else if(s == "\$tType") PARSER_STATE->parseError("Type of types `\$tType' cannot be used here"); else PARSER_STATE->parseError("unknown defined type `" + s + "'"); } - | LOWER_WORD - { type = PARSER_STATE->getSort(AntlrInput::tokenText($LOWER_WORD)); } + | atomicWord[name] + { type = PARSER_STATE->getSort(name); } ; /***********************************************/ diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index aa5849960..d75ec2126 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -1076,6 +1076,10 @@ void Smt2Printer::toStream(std::ostream& out, const Model& m) const throw() { while( std::getline( c, ln ) ){ out << "; " << ln << std::endl; } + //print the model + out << "(model" << endl; + this->Printer::toStream(out, m); + out << ")" << endl; //print the heap model, if it exists Expr h, neq; if( m.getHeapModel( h, neq ) ){ @@ -1085,10 +1089,6 @@ void Smt2Printer::toStream(std::ostream& out, const Model& m) const throw() { out << neq << endl; out << ")" << std::endl; } - //print the model - out << "(model" << endl; - this->Printer::toStream(out, m); - out << ")" << endl; } diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index edb92bb1b..6b89c3524 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -436,30 +436,32 @@ void Region::debugPrint( const char* c, bool incClique ) { } } } - Debug( c ) << "Total disequal: " << d_total_diseq_external << " external," - << std::endl; - Debug( c ) << " " << d_total_diseq_internal << " internal." - << std::endl; + Debug( c ) << "Total disequal: " << d_total_diseq_external << " external,"; + Debug( c ) << " " << d_total_diseq_internal << " internal." << std::endl; if( incClique ){ - Debug( c ) << "Candidate clique members: " << std::endl; - Debug( c ) << " "; - for( NodeBoolMap::iterator it = d_testClique.begin(); - it != d_testClique.end(); ++ it ){ - if( (*it).second ){ - Debug( c ) << (*it).first << " "; + if( !d_testClique.empty() ){ + Debug( c ) << "Candidate clique members: " << std::endl; + Debug( c ) << " "; + for( NodeBoolMap::iterator it = d_testClique.begin(); + it != d_testClique.end(); ++ it ){ + if( (*it).second ){ + Debug( c ) << (*it).first << " "; + } } + Debug( c ) << ", size = " << d_testCliqueSize << std::endl; } - Debug( c ) << ", size = " << d_testCliqueSize << std::endl; - Debug( c ) << "Required splits: " << std::endl; - Debug( c ) << " "; - for( NodeBoolMap::iterator it = d_splits.begin(); it != d_splits.end(); - ++ it ){ - if( (*it).second ){ - Debug( c ) << (*it).first << " "; + if( !d_splits.empty() ){ + Debug( c ) << "Required splits: " << std::endl; + Debug( c ) << " "; + for( NodeBoolMap::iterator it = d_splits.begin(); it != d_splits.end(); + ++ it ){ + if( (*it).second ){ + Debug( c ) << (*it).first << " "; + } } + Debug( c ) << ", size = " << d_splitsSize << std::endl; } - Debug( c ) << ", size = " << d_splitsSize << std::endl; } } @@ -697,6 +699,12 @@ bool SortModel::areDisequal( Node a, Node b ) { void SortModel::check( Theory::Effort level, OutputChannel* out ){ if( level>=Theory::EFFORT_STANDARD && d_hasCard && !d_conflict ){ Debug("uf-ss") << "StrongSolverTheoryUF: Check " << level << " " << d_type << std::endl; + if( level==Theory::EFFORT_FULL ){ + Debug("fmf-full-check") << std::endl; + Debug("fmf-full-check") << "Full check for SortModel " << d_type << ", status : " << std::endl; + debugPrint("fmf-full-check"); + Debug("fmf-full-check") << std::endl; + } //Notice() << "StrongSolverTheoryUF: Check " << level << std::endl; if( d_reps<=(unsigned)d_cardinality ){ Debug("uf-ss-debug") << "We have " << d_reps << " representatives for type " << d_type << ", <= " << d_cardinality << std::endl; @@ -772,6 +780,7 @@ void SortModel::check( Theory::Effort level, OutputChannel* out ){ Node op = d_regions[i]->frontKey(); int sort_id = d_thss->getSortInference()->getSortId(op); if( sortsFound.find( sort_id )!=sortsFound.end() ){ + Debug("fmf-full-check") << "Combined regions " << i << " " << sortsFound[sort_id] << std::endl; combineRegions( sortsFound[sort_id], i ); recheck = true; break; @@ -786,6 +795,7 @@ void SortModel::check( Theory::Effort level, OutputChannel* out ){ for( int i=0; i<(int)d_regions_index; i++ ){ if( d_regions[i]->valid() ){ int fcr = forceCombineRegion( i, false ); + Debug("fmf-full-check") << "Combined regions " << i << " " << fcr << std::endl; Trace("uf-ss-debug") << "Combined regions " << i << " " << fcr << std::endl; if( options::ufssMode()==UF_SS_FULL || fcr!=-1 ){ recheck = true; @@ -1053,8 +1063,10 @@ int SortModel::forceCombineRegion( int ri, bool useDensity ){ return -1; }else{ //this region must merge with another - Debug("uf-ss-check-region") << "We must combine Region #" << ri << ". " << std::endl; - d_regions[ri]->debugPrint("uf-ss-check-region"); + if( Debug.isOn("uf-ss-check-region") ){ + Debug("uf-ss-check-region") << "We must combine Region #" << ri << ". " << std::endl; + d_regions[ri]->debugPrint("uf-ss-check-region"); + } //take region with maximum disequality density double maxScore = 0; int maxRegion = -1; @@ -1074,8 +1086,10 @@ int SortModel::forceCombineRegion( int ri, bool useDensity ){ } } if( maxRegion!=-1 ){ - Debug("uf-ss-check-region") << "Combine with region #" << maxRegion << ":" << std::endl; - d_regions[maxRegion]->debugPrint("uf-ss-check-region"); + if( Debug.isOn("uf-ss-check-region") ){ + Debug("uf-ss-check-region") << "Combine with region #" << maxRegion << ":" << std::endl; + d_regions[maxRegion]->debugPrint("uf-ss-check-region"); + } return combineRegions( ri, maxRegion ); } return -1; @@ -1525,31 +1539,32 @@ bool SortModel::doSendLemma( Node lem ) { } void SortModel::debugPrint( const char* c ){ - Debug( c ) << "-- Conflict Find:" << std::endl; - Debug( c ) << "Number of reps = " << d_reps << std::endl; - Debug( c ) << "Cardinality req = " << d_cardinality << std::endl; - unsigned debugReps = 0; - for( int i=0; i<(int)d_regions_index; i++ ){ - Region* region = d_regions[i]; - if( region->valid() ){ - Debug( c ) << "Region #" << i << ": " << std::endl; - region->debugPrint( c, true ); - Debug( c ) << std::endl; - for( Region::iterator it = region->begin(); it != region->end(); ++it ){ - if( it->second->valid() ){ - if( d_regions_map[ it->first ]!=i ){ - Debug( c ) << "***Bad regions map : " << it->first - << " " << d_regions_map[ it->first ].get() << std::endl; + if( Debug.isOn( c ) ){ + Debug( c ) << "Number of reps = " << d_reps << std::endl; + Debug( c ) << "Cardinality req = " << d_cardinality << std::endl; + unsigned debugReps = 0; + for( unsigned i=0; ivalid() ){ + Debug( c ) << "Region #" << i << ": " << std::endl; + region->debugPrint( c, true ); + Debug( c ) << std::endl; + for( Region::iterator it = region->begin(); it != region->end(); ++it ){ + if( it->second->valid() ){ + if( d_regions_map[ it->first ]!=(int)i ){ + Debug( c ) << "***Bad regions map : " << it->first + << " " << d_regions_map[ it->first ].get() << std::endl; + } } } + debugReps += region->getNumReps(); } - debugReps += region->getNumReps(); } - } - if( debugReps!=d_reps ){ - Debug( c ) << "***Bad reps: " << d_reps << ", " - << "actual = " << debugReps << std::endl; + if( debugReps!=d_reps ){ + Debug( c ) << "***Bad reps: " << d_reps << ", " + << "actual = " << debugReps << std::endl; + } } } diff --git a/test/regress/regress0/sep/quant_wand.smt2 b/test/regress/regress0/sep/quant_wand.smt2 index 9c38fb405..8a69c10c4 100644 --- a/test/regress/regress0/sep/quant_wand.smt2 +++ b/test/regress/regress0/sep/quant_wand.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi-all +; COMMAND-LINE: --full-saturate-quant ; EXPECT: unsat (set-logic ALL_SUPPORTED) (set-info :status unsat)