Context Navigation

SatisfyAssertions.cpp@ 09da82d

Visit:

ADT arm-eh ast-experimental enum forall-pointer-decay jacob/cs343-translation new-ast-unique-expr pthread-emulation qualifiedEnum

Last change on this file since 09da82d was 7583c02, checked in by Fangren Yu <f37yu@…>, 5 years ago

partially improve #226: resolver environment size reduced to O(n)

generated code still has exponential size. should cache resolved implicits
and reuse thunks to reduce generated code size.
assertion fails cannot exit early and may have a minor performance
reduction.

Property mode set to 100644

File size: 19.3 KB

Rev	Line
[396037d]	1	//
	2	// Cforall Version 1.0.0 Copyright (C) 2015 University of Waterloo
	3	//
	4	// The contents of this file are covered under the licence agreement in the
	5	// file "LICENCE" distributed with Cforall.
	6	//
	7	// SatisfyAssertions.cpp --
	8	//
	9	// Author : Aaron B. Moss
	10	// Created On : Mon Jun 10 17:45:00 2019
[cf32116]	11	// Last Modified By : Andrew Beach
	12	// Last Modified On : Tue Oct 1 13:56:00 2019
	13	// Update Count : 2
[396037d]	14	//
	15
	16	#include "SatisfyAssertions.hpp"
	17
[b69233ac]	18	#include <algorithm>
[396037d]	19	#include <cassert>
[b69233ac]	20	#include <sstream>
	21	#include <string>
	22	#include <unordered_map>
	23	#include <vector>
	24
	25	#include "Candidate.hpp"
	26	#include "CandidateFinder.hpp"
	27	#include "Cost.h"
	28	#include "RenameVars.h"
	29	#include "typeops.h"
	30	#include "Unify.h"
	31	#include "AST/Decl.hpp"
	32	#include "AST/Expr.hpp"
	33	#include "AST/Node.hpp"
	34	#include "AST/Pass.hpp"
	35	#include "AST/Print.hpp"
	36	#include "AST/SymbolTable.hpp"
	37	#include "AST/TypeEnvironment.hpp"
	38	#include "Common/FilterCombos.h"
	39	#include "Common/Indenter.h"
	40	#include "GenPoly/GenPoly.h"
	41	#include "SymTab/Mangler.h"
[396037d]	42
	43	namespace ResolvExpr {
	44
[b69233ac]	45	// in CandidateFinder.cpp; unique ID for assertion satisfaction
	46	extern UniqueId globalResnSlot;
	47
	48	namespace {
	49	/// Post-unification assertion satisfaction candidate
	50	struct AssnCandidate {
	51	ast::SymbolTable::IdData cdata; ///< Satisfying declaration
	52	ast::ptr< ast::Type > adjType; ///< Satisfying type
	53	ast::TypeEnvironment env; ///< Post-unification environment
	54	ast::AssertionSet have; ///< Post-unification have-set
	55	ast::AssertionSet need; ///< Post-unification need-set
	56	ast::OpenVarSet open; ///< Post-unification open-var-set
	57	ast::UniqueId resnSlot; ///< Slot for any recursive assertion IDs
	58
	59	AssnCandidate(
	60	const ast::SymbolTable::IdData c, const ast::Type * at, ast::TypeEnvironment && e,
	61	ast::AssertionSet && h, ast::AssertionSet && n, ast::OpenVarSet && o, ast::UniqueId rs )
	62	: cdata( c ), adjType( at ), env( std::move( e ) ), have( std::move( h ) ),
	63	need( std::move( n ) ), open( std::move( o ) ), resnSlot( rs ) {}
	64	};
	65
	66	/// List of assertion satisfaction candidates
	67	using AssnCandidateList = std::vector< AssnCandidate >;
	68
	69	/// Reference to a single deferred item
	70	struct DeferRef {
[3e5dd913]	71	const ast::VariableExpr * expr;
[b69233ac]	72	const ast::AssertionSetValue & info;
	73	const AssnCandidate & match;
	74	};
	75
	76	/// Wrapper for the deferred items from a single assertion satisfaction.
	77	/// Acts like an indexed list of DeferRef
	78	struct DeferItem {
[3e5dd913]	79	const ast::VariableExpr * expr;
[b69233ac]	80	const ast::AssertionSetValue & info;
	81	AssnCandidateList matches;
	82
	83	DeferItem(
[3e5dd913]	84	const ast::VariableExpr * d, const ast::AssertionSetValue & i, AssnCandidateList && ms )
	85	: expr( d ), info( i ), matches( std::move( ms ) ) {}
[b69233ac]	86
	87	bool empty() const { return matches.empty(); }
	88
	89	AssnCandidateList::size_type size() const { return matches.size(); }
	90
[3e5dd913]	91	DeferRef operator[] ( unsigned i ) const { return { expr, info, matches[i] }; }
[b69233ac]	92	};
	93
	94	/// List of deferred satisfaction items
	95	using DeferList = std::vector< DeferItem >;
	96
	97	/// Set of assertion satisfactions, grouped by resolution ID
	98	using InferCache = std::unordered_map< ast::UniqueId, ast::InferredParams >;
	99
	100	/// Lexicographically-ordered vector of costs.
	101	/// Lexicographic order comes from default operator< on std::vector.
	102	using CostVec = std::vector< Cost >;
	103
	104	/// Flag for state iteration
	105	enum IterateFlag { IterateState };
	106
	107	/// Intermediate state for satisfying a set of assertions
	108	struct SatState {
	109	CandidateRef cand; ///< Candidate assertion is rooted on
	110	ast::AssertionList need; ///< Assertions to find
	111	ast::AssertionSet newNeed; ///< Recursive assertions from current satisfied assertions
	112	DeferList deferred; ///< Deferred matches
	113	InferCache inferred; ///< Cache of already-inferred assertions
	114	CostVec costs; ///< Disambiguating costs of recursive assertion satisfaction
	115	ast::SymbolTable symtab; ///< Name lookup (depends on previous assertions)
	116
	117	/// Initial satisfaction state for a candidate
	118	SatState( CandidateRef & c, const ast::SymbolTable & syms )
	119	: cand( c ), need(), newNeed(), deferred(), inferred(), costs{ Cost::zero },
	120	symtab( syms ) { need.swap( c->need ); }
	121
	122	/// Update satisfaction state for next step after previous state
	123	SatState( SatState && o, IterateFlag )
	124	: cand( std::move( o.cand ) ), need( o.newNeed.begin(), o.newNeed.end() ), newNeed(),
	125	deferred(), inferred( std::move( o.inferred ) ), costs( std::move( o.costs ) ),
	126	symtab( o.symtab ) { costs.emplace_back( Cost::zero ); }
	127
	128	/// Field-wise next step constructor
	129	SatState(
	130	CandidateRef && c, ast::AssertionSet && nn, InferCache && i, CostVec && cs,
	131	ast::SymbolTable && syms )
	132	: cand( std::move( c ) ), need( nn.begin(), nn.end() ), newNeed(), deferred(),
	133	inferred( std::move( i ) ), costs( std::move( cs ) ), symtab( std::move( syms ) )
	134	{ costs.emplace_back( Cost::zero ); }
	135	};
	136
	137	/// Adds a captured assertion to the symbol table
	138	void addToSymbolTable( const ast::AssertionSet & have, ast::SymbolTable & symtab ) {
	139	for ( auto & i : have ) {
[3e5dd913]	140	if ( i.second.isUsed ) { symtab.addId( i.first->var ); }
[b69233ac]	141	}
	142	}
	143
	144	/// Binds a single assertion, updating satisfaction state
	145	void bindAssertion(
[3e5dd913]	146	const ast::VariableExpr * expr, const ast::AssertionSetValue & info, CandidateRef & cand,
[b69233ac]	147	AssnCandidate & match, InferCache & inferred
	148	) {
	149	const ast::DeclWithType * candidate = match.cdata.id;
	150	assertf( candidate->uniqueId,
	151	"Assertion candidate does not have a unique ID: %s", toString( candidate ).c_str() );
	152
	153	ast::Expr * varExpr = match.cdata.combine( cand->expr->location, cand->cvtCost );
	154	varExpr->result = match.adjType;
	155	if ( match.resnSlot ) { varExpr->inferred.resnSlots().emplace_back( match.resnSlot ); }
	156
	157	// place newly-inferred assertion in proper location in cache
[3e5dd913]	158	inferred[ info.resnSlot ][ expr->var->uniqueId ] = ast::ParamEntry{
	159	candidate->uniqueId, candidate, match.adjType, expr->result, varExpr };
[b69233ac]	160	}
	161
	162	/// Satisfy a single assertion
	163	bool satisfyAssertion( ast::AssertionList::value_type & assn, SatState & sat ) {
	164	// skip unused assertions
	165	if ( ! assn.second.isUsed ) return true;
	166
	167	// find candidates that unify with the desired type
	168	AssnCandidateList matches;
[e5c3811]	169
	170	std::vector<ast::SymbolTable::IdData> candidates;
[3e5dd913]	171	auto kind = ast::SymbolTable::getSpecialFunctionKind(assn.first->var->name);
[e5c3811]	172	if (kind != ast::SymbolTable::SpecialFunctionKind::NUMBER_OF_KINDS) {
	173	// prefilter special decls by argument type, if already known
[3e5dd913]	174	ast::ptr<ast::Type> thisArgType = assn.first->result.strict_as<ast::PointerType>()->base
[e5c3811]	175	.strict_as<ast::FunctionType>()->params[0]
	176	.strict_as<ast::ReferenceType>()->base;
	177	sat.cand->env.apply(thisArgType);
	178
	179	std::string otypeKey = "";
	180	if (thisArgType.as<ast::PointerType>()) otypeKey = Mangle::Encoding::pointer;
	181	else if (!isUnboundType(thisArgType)) otypeKey = Mangle::mangle(thisArgType, Mangle::Type \| Mangle::NoGenericParams);
	182
	183	candidates = sat.symtab.specialLookupId(kind, otypeKey);
	184	}
	185	else {
[3e5dd913]	186	candidates = sat.symtab.lookupId(assn.first->var->name);
[e5c3811]	187	}
	188	for ( const ast::SymbolTable::IdData & cdata : candidates ) {
[b69233ac]	189	const ast::DeclWithType * candidate = cdata.id;
	190
[2fb35df]	191	// ignore deleted candidates.
	192	// NOTE: this behavior is different from main resolver.
	193	// further investigations might be needed to determine
	194	// if we should implement the same rule here
	195	// (i.e. error if unique best match is deleted)
[5b9a0ae]	196	if (candidate->isDeleted && candidate->linkage == ast::Linkage::AutoGen) continue;
[2fb35df]	197
[b69233ac]	198	// build independent unification context for candidate
	199	ast::AssertionSet have, newNeed;
	200	ast::TypeEnvironment newEnv{ sat.cand->env };
	201	ast::OpenVarSet newOpen{ sat.cand->open };
[3e5dd913]	202	ast::ptr< ast::Type > toType = assn.first->result;
[b69233ac]	203	ast::ptr< ast::Type > adjType =
[7583c02]	204	renameTyVars( adjustExprType( candidate->get_type(), newEnv, sat.symtab ), GEN_USAGE, false );
[b69233ac]	205
	206	// only keep candidates which unify
	207	if ( unify( toType, adjType, newEnv, newNeed, have, newOpen, sat.symtab ) ) {
	208	// set up binding slot for recursive assertions
	209	ast::UniqueId crntResnSlot = 0;
	210	if ( ! newNeed.empty() ) {
	211	crntResnSlot = ++globalResnSlot;
	212	for ( auto & a : newNeed ) { a.second.resnSlot = crntResnSlot; }
	213	}
	214
	215	matches.emplace_back(
[07d867b]	216	cdata, adjType, std::move( newEnv ), std::move( have ), std::move( newNeed ),
[b69233ac]	217	std::move( newOpen ), crntResnSlot );
	218	}
	219	}
	220
	221	// break if no satisfying match
	222	if ( matches.empty() ) return false;
	223
	224	// defer if too many satisfying matches
	225	if ( matches.size() > 1 ) {
	226	sat.deferred.emplace_back( assn.first, assn.second, std::move( matches ) );
	227	return true;
	228	}
	229
	230	// otherwise bind unique match in ongoing scope
	231	AssnCandidate & match = matches.front();
	232	addToSymbolTable( match.have, sat.symtab );
	233	sat.newNeed.insert( match.need.begin(), match.need.end() );
	234	sat.cand->env = std::move( match.env );
	235	sat.cand->open = std::move( match.open );
	236
	237	bindAssertion( assn.first, assn.second, sat.cand, match, sat.inferred );
	238	return true;
	239	}
	240
	241	/// Map of candidate return types to recursive assertion satisfaction costs
	242	using PruneMap = std::unordered_map< std::string, CostVec >;
	243
	244	/// Gets the pruning key for a candidate (derived from environment-adjusted return type)
	245	std::string pruneKey( const Candidate & cand ) {
	246	ast::ptr< ast::Type > resType = cand.expr->result;
	247	cand.env.apply( resType );
	248	return Mangle::mangle( resType, Mangle::typeMode() );
	249	}
	250
	251	/// Associates inferred parameters with an expression
	252	struct InferMatcher final {
	253	InferCache & inferred;
	254
	255	InferMatcher( InferCache & inferred ) : inferred( inferred ) {}
	256
[81da70a5]	257	const ast::Expr * postvisit( const ast::Expr * expr ) {
[b69233ac]	258	// Skip if no slots to find
[07d867b]	259	if ( !expr->inferred.hasSlots() ) return expr;
	260	// if ( expr->inferred.mode != ast::Expr::InferUnion::Slots ) return expr;
	261	std::vector<UniqueId> missingSlots;
[b69233ac]	262	// find inferred parameters for resolution slots
[07d867b]	263	ast::InferredParams * newInferred = new ast::InferredParams();
[b69233ac]	264	for ( UniqueId slot : expr->inferred.resnSlots() ) {
	265	// fail if no matching assertions found
	266	auto it = inferred.find( slot );
	267	if ( it == inferred.end() ) {
[cdacb73]	268	// std::cerr << "missing assertion " << slot << std::endl;
[07d867b]	269	missingSlots.push_back(slot);
[81da70a5]	270	continue;
[b69233ac]	271	}
	272
	273	// place inferred parameters into new map
	274	for ( auto & entry : it->second ) {
	275	// recurse on inferParams of resolved expressions
[81da70a5]	276	entry.second.expr = postvisit( entry.second.expr );
[07d867b]	277	auto res = newInferred->emplace( entry );
[b69233ac]	278	assert( res.second && "all assertions newly placed" );
	279	}
	280	}
	281
	282	ast::Expr * ret = mutate( expr );
[07d867b]	283	ret->inferred.set_inferParams( newInferred );
	284	if (!missingSlots.empty()) ret->inferred.resnSlots() = missingSlots;
[b69233ac]	285	return ret;
	286	}
	287	};
	288
	289	/// Replace ResnSlots with InferParams and add alternative to output list, if it meets pruning
	290	/// threshold.
	291	void finalizeAssertions(
	292	CandidateRef & cand, InferCache & inferred, PruneMap & thresholds, CostVec && costs,
	293	CandidateList & out
	294	) {
	295	// prune if cheaper alternative for same key has already been generated
	296	std::string key = pruneKey( *cand );
	297	auto it = thresholds.find( key );
	298	if ( it != thresholds.end() ) {
	299	if ( it->second < costs ) return;
	300	} else {
	301	thresholds.emplace_hint( it, key, std::move( costs ) );
	302	}
	303
	304	// replace resolution slots with inferred parameters, add to output
	305	ast::Pass< InferMatcher > matcher{ inferred };
	306	cand->expr = cand->expr->accept( matcher );
	307	out.emplace_back( cand );
	308	}
	309
	310	/// Combo iterator that combines candidates into an output list, merging their environments.
	311	/// Rejects an appended candidate if environments cannot be merged. See `Common/FilterCombos.h`
	312	/// for description of "combo iterator".
	313	class CandidateEnvMerger {
	314	/// Current list of merged candidates
	315	std::vector< DeferRef > crnt;
	316	/// Stack of environments to support backtracking
	317	std::vector< ast::TypeEnvironment > envs;
	318	/// Stack of open variables to support backtracking
	319	std::vector< ast::OpenVarSet > opens;
	320	/// Symbol table to use for merges
	321	const ast::SymbolTable & symtab;
	322
	323	public:
	324	/// The merged environment/open variables and the list of candidates
	325	struct OutType {
	326	ast::TypeEnvironment env;
	327	ast::OpenVarSet open;
	328	std::vector< DeferRef > assns;
	329	Cost cost;
	330
[cf32116]	331	OutType(
	332	const ast::TypeEnvironment & e, const ast::OpenVarSet & o,
[b69233ac]	333	const std::vector< DeferRef > & as, const ast::SymbolTable & symtab )
	334	: env( e ), open( o ), assns( as ), cost( Cost::zero ) {
	335	// compute combined conversion cost
	336	for ( const DeferRef & assn : assns ) {
	337	// compute conversion cost from satisfying decl to assertion
[cf32116]	338	cost += computeConversionCost(
[3e5dd913]	339	assn.match.adjType, assn.expr->result, false, symtab, env );
[cf32116]	340
[b69233ac]	341	// mark vars+specialization on function-type assertions
[cf32116]	342	const ast::FunctionType * func =
[b69233ac]	343	GenPoly::getFunctionType( assn.match.cdata.id->get_type() );
	344	if ( ! func ) continue;
	345
[954c954]	346	for ( const auto & param : func->params ) {
	347	cost.decSpec( specCost( param ) );
[b69233ac]	348	}
[cf32116]	349
[b69233ac]	350	cost.incVar( func->forall.size() );
[cf32116]	351
[3e5dd913]	352	cost.decSpec( func->assertions.size() );
[b69233ac]	353	}
	354	}
	355
	356	bool operator< ( const OutType & o ) const { return cost < o.cost; }
	357	};
	358
[cf32116]	359	CandidateEnvMerger(
	360	const ast::TypeEnvironment & env, const ast::OpenVarSet & open,
[b69233ac]	361	const ast::SymbolTable & syms )
	362	: crnt(), envs{ env }, opens{ open }, symtab( syms ) {}
	363
	364	bool append( DeferRef i ) {
	365	ast::TypeEnvironment env = envs.back();
	366	ast::OpenVarSet open = opens.back();
	367	mergeOpenVars( open, i.match.open );
	368
	369	if ( ! env.combine( i.match.env, open, symtab ) ) return false;
	370
	371	crnt.emplace_back( i );
	372	envs.emplace_back( std::move( env ) );
	373	opens.emplace_back( std::move( open ) );
	374	return true;
	375	}
	376
	377	void backtrack() {
	378	crnt.pop_back();
	379	envs.pop_back();
	380	opens.pop_back();
	381	}
	382
	383	OutType finalize() { return { envs.back(), opens.back(), crnt, symtab }; }
	384	};
	385
	386	/// Limit to depth of recursion of assertion satisfaction
	387	static const int recursionLimit = 4;
	388	/// Maximum number of simultaneously-deferred assertions to attempt concurrent satisfaction of
	389	static const int deferLimit = 10;
	390	} // anonymous namespace
	391
[396037d]	392	void satisfyAssertions(
[b69233ac]	393	CandidateRef & cand, const ast::SymbolTable & symtab, CandidateList & out,
[396037d]	394	std::vector<std::string> & errors
	395	) {
[b69233ac]	396	// finish early if no assertions to satisfy
	397	if ( cand->need.empty() ) {
	398	out.emplace_back( cand );
	399	return;
	400	}
	401
	402	// build list of possible combinations of satisfying declarations
	403	std::vector< SatState > sats{ SatState{ cand, symtab } };
	404	std::vector< SatState > nextSats{};
	405
	406	// pruning thresholds by result type of output candidates.
	407	// Candidates should be generated in sorted order, so no need to retroactively prune
	408	PruneMap thresholds;
	409
	410	// satisfy assertions in breadth-first order over the recursion tree of assertion satisfaction.
	411	// Stop recursion at a limited number of levels deep to avoid infinite loops.
	412	for ( unsigned level = 0; level < recursionLimit; ++level ) {
	413	// for each current mutually-compatible set of assertions
	414	for ( SatState & sat : sats ) {
	415	// stop this branch if a better option is already found
	416	auto it = thresholds.find( pruneKey( *sat.cand ) );
	417	if ( it != thresholds.end() && it->second < sat.costs ) goto nextSat;
	418
[7583c02]	419	// should a limit be imposed? worst case here is O(n^2) but very unlikely to happen.
	420	for (unsigned resetCount = 0; ; ++resetCount) {
	421	ast::AssertionList next;
	422	resetTyVarRenaming();
	423	// make initial pass at matching assertions
	424	for ( auto & assn : sat.need ) {
	425	// fail early if any assertion is not satisfiable
	426	if ( ! satisfyAssertion( assn, sat ) ) {
	427	next.emplace_back(assn);
	428	// goto nextSat;
	429	}
	430	}
	431	// success
	432	if (next.empty()) break;
	433	// fail if nothing resolves
	434	else if (next.size() == sat.need.size()) {
[b69233ac]	435	Indenter tabs{ 3 };
	436	std::ostringstream ss;
	437	ss << tabs << "Unsatisfiable alternative:\n";
	438	print( ss, *sat.cand, ++tabs );
	439	ss << (tabs-1) << "Could not satisfy assertion:\n";
[7583c02]	440	ast::print( ss, next[0].first, tabs );
[b69233ac]	441
	442	errors.emplace_back( ss.str() );
	443	goto nextSat;
	444	}
[7583c02]	445	sat.need = std::move(next);
[b69233ac]	446	}
	447
	448	if ( sat.deferred.empty() ) {
	449	// either add successful match or push back next state
	450	if ( sat.newNeed.empty() ) {
	451	finalizeAssertions(
	452	sat.cand, sat.inferred, thresholds, std::move( sat.costs ), out );
	453	} else {
	454	nextSats.emplace_back( std::move( sat ), IterateState );
	455	}
	456	} else if ( sat.deferred.size() > deferLimit ) {
	457	// too many deferred assertions to attempt mutual compatibility
	458	Indenter tabs{ 3 };
	459	std::ostringstream ss;
	460	ss << tabs << "Unsatisfiable alternative:\n";
	461	print( ss, *sat.cand, ++tabs );
	462	ss << (tabs-1) << "Too many non-unique satisfying assignments for assertions:\n";
	463	for ( const auto & d : sat.deferred ) {
[3e5dd913]	464	ast::print( ss, d.expr, tabs );
[b69233ac]	465	}
	466
	467	errors.emplace_back( ss.str() );
	468	goto nextSat;
	469	} else {
	470	// combine deferred assertions by mutual compatibility
	471	std::vector< CandidateEnvMerger::OutType > compatible = filterCombos(
	472	sat.deferred, CandidateEnvMerger{ sat.cand->env, sat.cand->open, sat.symtab } );
	473
	474	// fail early if no mutually-compatible assertion satisfaction
	475	if ( compatible.empty() ) {
	476	Indenter tabs{ 3 };
	477	std::ostringstream ss;
	478	ss << tabs << "Unsatisfiable alternative:\n";
	479	print( ss, *sat.cand, ++tabs );
	480	ss << (tabs-1) << "No mutually-compatible satisfaction for assertions:\n";
	481	for ( const auto& d : sat.deferred ) {
[3e5dd913]	482	ast::print( ss, d.expr, tabs );
[b69233ac]	483	}
	484
	485	errors.emplace_back( ss.str() );
	486	goto nextSat;
	487	}
	488
	489	// sort by cost (for overall pruning order)
	490	std::sort( compatible.begin(), compatible.end() );
	491
	492	// process mutually-compatible combinations
	493	for ( auto & compat : compatible ) {
	494	// set up next satisfaction state
	495	CandidateRef nextCand = std::make_shared<Candidate>(
	496	sat.cand->expr, std::move( compat.env ), std::move( compat.open ),
	497	ast::AssertionSet{} /* need moved into satisfaction state */,
	498	sat.cand->cost, sat.cand->cvtCost );
	499
	500	ast::AssertionSet nextNewNeed{ sat.newNeed };
	501	InferCache nextInferred{ sat.inferred };
	502
	503	CostVec nextCosts{ sat.costs };
	504	nextCosts.back() += compat.cost;
	505
	506	ast::SymbolTable nextSymtab{ sat.symtab };
	507
	508	// add compatible assertions to new satisfaction state
	509	for ( DeferRef r : compat.assns ) {
	510	AssnCandidate match = r.match;
	511	addToSymbolTable( match.have, nextSymtab );
	512	nextNewNeed.insert( match.need.begin(), match.need.end() );
	513
[3e5dd913]	514	bindAssertion( r.expr, r.info, nextCand, match, nextInferred );
[b69233ac]	515	}
	516
	517	// either add successful match or push back next state
	518	if ( nextNewNeed.empty() ) {
	519	finalizeAssertions(
	520	nextCand, nextInferred, thresholds, std::move( nextCosts ), out );
	521	} else {
	522	nextSats.emplace_back(
	523	std::move( nextCand ), std::move( nextNewNeed ),
	524	std::move( nextInferred ), std::move( nextCosts ),
	525	std::move( nextSymtab ) );
	526	}
	527	}
	528	}
	529	nextSat:; }
	530
	531	// finish or reset for next round
	532	if ( nextSats.empty() ) return;
	533	sats.swap( nextSats );
	534	nextSats.clear();
	535	}
	536
	537	// exceeded recursion limit if reaches here
	538	if ( out.empty() ) {
	539	SemanticError( cand->expr->location, "Too many recursive assertions" );
	540	}
[396037d]	541	}
	542
	543	} // namespace ResolvExpr
	544
	545	// Local Variables: //
	546	// tab-width: 4 //
	547	// mode: c++ //
	548	// compile-command: "make install" //
[cf32116]	549	// End: //

Note: See TracBrowser for help on using the repository browser.

Context Navigation

source: src/ResolvExpr/SatisfyAssertions.cpp@ 09da82d

Download in other formats: