throw Unimplemented("unknown kind of goal");
throw Exception("unknown kind of goal");
static bool add_goal(const OpenConditionChain*& open_conds,		     size_t& num_open_conds, BindingList& new_bindings,		     const Formula& goal, size_t step_id,		     const Reason& reason, bool test_only = false) {  if (goal.tautology()) {    return true;  } else if (goal.contradiction()) {    return false;  }  deque<const Formula*> goals(1, &goal);  while (!goals.empty()) {    const Formula* goal = goals.back();    goals.pop_back();    const Conjunction* conj = dynamic_cast<const Conjunction*>(goal);    if (conj != NULL) {      const FormulaList& gs = conj->conjuncts();      for (FormulaListIter fi = gs.begin(); fi != gs.end(); fi++) {	if (params->reverse_open_conditions) {	  goals.push_front(*fi);	} else {	  goals.push_back(*fi);	}      }    } else {      const Literal* literal = dynamic_cast<const Literal*>(goal);      if (literal != NULL) {	if (!test_only	    && !(params->strip_static_preconditions()		 && domain->static_predicate(literal->predicate()))) {	  open_conds =	    new OpenConditionChain(OpenCondition(step_id, *goal, reason),				   open_conds);	}	num_open_conds++;      } else {	const Disjunction* disj = dynamic_cast<const Disjunction*>(goal);	if (disj != NULL) {	  if (!test_only) {	    open_conds =	      new OpenConditionChain(OpenCondition(step_id, *goal, reason),				     open_conds);	  }	  num_open_conds++;	} else {	  const BindingLiteral* bl = dynamic_cast<const BindingLiteral*>(goal);	  if (bl != NULL) {	    bool is_eq = (typeid(*bl) == typeid(Equality));	    bool added = false;	    const Variable* var = dynamic_cast<const Variable*>(&bl->term1());	    if (var != NULL) {	      /* The first term is a variable. */	      new_bindings.push_back(Binding(*var, bl->step_id1(step_id),					     bl->term2(),					     bl->step_id2(step_id),					     is_eq, reason));	      added = true;	    } else {	      var = dynamic_cast<const Variable*>(&bl->term2());	      if (var != NULL) {		/* The second term is a variable. */		new_bindings.push_back(Binding(*var, bl->step_id2(step_id),					       bl->term1(),					       bl->step_id1(step_id),					       is_eq, reason));		added = true;	      } else if ((is_eq && bl->term1() != bl->term2())			 || (!is_eq && bl->term1() == bl->term2())) {		/* Both terms are names, and the binding is inconsistent. */		return false;	      }	    }	    if (added) {#ifdef BRANCH_ON_INEQUALITY	      const Inequality* neq = dynamic_cast<const Inequality*>(bl);	      if (params->domain_constraints		  && neq != NULL && typeid(bl->term1) == typeid(bl->term2)) {		/* Both terms are variables, so handle specially. */		if (!test_only) {		  open_conds =		    new OpenConditionChain(OpenCondition(step_id, *neq,							 reason),					   open_conds);		  num_open_conds++;		}		new_bindings.pop_back();	      }#endif	    }	  } else {	    const ExistsFormula* exists =	      dynamic_cast<const ExistsFormula*>(goal);	    if (exists != NULL) {	      if (params->reverse_open_conditions) {		goals.push_front(&exists->body());	      } else {		goals.push_back(&exists->body());	      }	    } else if (dynamic_cast<const ForallFormula*>(goal) != NULL) {	      throw Unimplemented("adding universally quantified goal");	    } else {	      throw Unimplemented("unknown kind of goal");	    }	  }	}      }    }  }  return true;}